author  wenzelm 
Sat, 28 Jul 2007 20:40:22 +0200  
changeset 24019  67bde7cfcf10 
parent 22708  fff918feff45 
child 26342  0f65fa163304 
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 **) 

22708  68 
datatype tnam' = HasFoo'  Base'  Ext'  Main' 
69 
datatype vnam' = arr'  vee'  z'  e' 

70 
datatype label' = lab1' 

12854  71 

72 
consts 

73 

22708  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 

12854  78 
to tnam, vname and label **) 
79 

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

12854  83 

84 

22708  85 
surj_tnam': "\<exists>m. n = tnam' m" 
86 
surj_vnam': "\<exists>m. n = vnam' m" 

87 
surj_label':" \<exists>m. n = label' m" 

12854  88 

20769  89 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

90 
HasFoo :: qtname where 
22708  91 
"HasFoo == \<lparr>pid=java_lang,tid=TName (tnam' HasFoo')\<rparr>" 
20769  92 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

93 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

94 
Base :: qtname where 
22708  95 
"Base == \<lparr>pid=java_lang,tid=TName (tnam' Base')\<rparr>" 
20769  96 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

97 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

98 
Ext :: qtname where 
22708  99 
"Ext == \<lparr>pid=java_lang,tid=TName (tnam' Ext')\<rparr>" 
20769  100 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

101 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

102 
Main :: qtname where 
22708  103 
"Main == \<lparr>pid=java_lang,tid=TName (tnam' Main')\<rparr>" 
20769  104 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

105 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

106 
arr :: vname where 
22708  107 
"arr == (vnam' arr')" 
20769  108 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

109 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

110 
vee :: vname where 
22708  111 
"vee == (vnam' vee')" 
20769  112 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

113 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

114 
z :: vname where 
22708  115 
"z == (vnam' z')" 
20769  116 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

117 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

118 
e :: vname where 
22708  119 
"e == (vnam' e')" 
20769  120 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

121 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

122 
lab1:: label where 
22708  123 
"lab1 == label' lab1'" 
12854  124 

125 

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

127 
by (simp add: Object_def) 

128 

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

130 
by (simp add: Object_def) 

131 

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

132 
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

133 
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

134 

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

137 

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

139 
by (simp add: SXcpt_def) 

140 

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

142 
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

143 

12854  144 
section "classes and interfaces" 
145 

146 
defs 

147 

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

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

150 

151 
consts 

152 

153 
foo :: mname 

154 

155 
constdefs 

156 

157 
foo_sig :: sig 

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

159 

160 
foo_mhead :: mhead 

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

162 

163 
constdefs 

164 

165 
Base_foo :: mdecl 

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

167 
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

168 

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

169 
constdefs 
12854  170 
Ext_foo :: mdecl 
171 
"Ext_foo \<equiv> (foo_sig, 

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

173 
mbody=\<lparr>lcls=[] 

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

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

175 
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

176 
Return (Lit Null)\<rparr> 
12854  177 
\<rparr>)" 
178 

179 
constdefs 

180 

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

181 
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

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

18551  184 
BaseCl :: "class" 
12854  185 
"BaseCl \<equiv> \<lparr>access=Public, 
186 
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), 

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

188 
methods=[Base_foo], 

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

189 
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

190 
:=New (PrimT Boolean)[Lit (Intg 2)]), 
12854  191 
super=Object, 
192 
superIfs=[HasFoo]\<rparr>" 

193 

18551  194 
ExtCl :: "class" 
12854  195 
"ExtCl \<equiv> \<lparr>access=Public, 
196 
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 

197 
methods=[Ext_foo], 

198 
init=Skip, 

199 
super=Base, 

200 
superIfs=[]\<rparr>" 

201 

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

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

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

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

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

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

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

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

210 

12854  211 
constdefs 
212 

213 
HasFooInt :: iface 

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

215 

216 
Ifaces ::"idecl list" 

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

218 

219 
"Classes" ::"cdecl list" 

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

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

222 
lemmas table_classes_defs = 

223 
Classes_def standard_classes_def ObjectC_def SXcptC_def 

224 

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

226 
apply (unfold Ifaces_def) 

227 
apply (simp (no_asm)) 

228 
done 

229 

230 
lemma table_classes_Object [simp]: 

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

232 
,methods=Object_mdecls 

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

234 
apply (unfold table_classes_defs) 

235 
apply (simp (no_asm) add:Object_def) 

236 
done 

237 

238 
lemma table_classes_SXcpt [simp]: 

239 
"table_of Classes (SXcpt xn) 

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

241 
init=Skip, 

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

243 
superIfs=[]\<rparr>" 

244 
apply (unfold table_classes_defs) 

245 
apply (induct_tac xn) 

246 
apply (simp add: Object_def SXcpt_def)+ 

247 
done 

248 

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

250 
apply (unfold table_classes_defs) 

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

252 
done 

253 

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

255 
apply (unfold table_classes_defs ) 

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

257 
done 

258 

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

260 
apply (unfold table_classes_defs ) 

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

262 
done 

263 

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

264 
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

265 
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

266 
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

267 
done 
12854  268 

269 
section "program" 

270 

20769  271 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

272 
tprg :: prog where 
20769  273 
"tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>" 
12854  274 

275 
constdefs 

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

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

278 
\<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null])) 
12854  279 
\<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

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

281 
(Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)" 
12854  282 

283 

284 
section "wellstructuredness" 

285 

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

287 
apply (auto dest!: tranclD subcls1D) 

288 
done 

289 

290 
lemma not_Throwable_subcls_SXcpt [elim!]: 

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

292 
apply (auto dest!: tranclD subcls1D) 

293 
apply (simp add: Object_def SXcpt_def) 

294 
done 

295 

296 
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 

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

298 
apply (auto dest!: tranclD subcls1D) 

299 
apply (drule rtranclD) 

300 
apply auto 

301 
done 

302 

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

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

305 
done 

306 

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

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

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

22708  310 
apply (rule_tac n1 = "tn" in surj_tnam' [THEN exE]) 
12854  311 
apply (erule ssubst) 
22708  312 
apply (rule tnam'.induct) 
12854  313 
apply safe 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

314 
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def) 
12854  315 
apply (drule rtranclD) 
316 
apply auto 

317 
done 

318 

319 

320 
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []" 

321 
apply (unfold ws_idecl_def) 

322 
apply (simp (no_asm)) 

323 
done 

324 

325 
lemma ws_cdecl_Object: "ws_cdecl tprg Object any" 

326 
apply (unfold ws_cdecl_def) 

327 
apply auto 

328 
done 

329 

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

331 
apply (unfold ws_cdecl_def) 

332 
apply auto 

333 
done 

334 

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

336 
apply (unfold ws_cdecl_def) 

337 
apply auto 

338 
done 

339 

340 
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object" 

341 
apply (unfold ws_cdecl_def) 

342 
apply auto 

343 
done 

344 

345 
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base" 

346 
apply (unfold ws_cdecl_def) 

347 
apply auto 

348 
done 

349 

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

350 
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

351 
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

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

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

354 

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

356 
ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main 
12854  357 

358 
declare not_Object_subcls_any [rule del] 

359 
not_Throwable_subcls_SXcpt [rule del] 

360 
not_SXcpt_n_subcls_SXcpt_n [rule del] 

361 
not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del] 

362 

363 
lemma ws_idecl_all: 

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

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

366 
apply (auto intro!: ws_idecl_HasFoo) 

367 
done 

368 

369 
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

370 
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def) 
12854  371 
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
372 
SXcptC_def) 

373 
done 

374 

375 
lemma ws_tprg: "ws_prog tprg" 

376 
apply (unfold ws_prog_def) 

377 
apply (auto intro!: ws_idecl_all ws_cdecl_all) 

378 
done 

379 

380 

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

382 

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

384 
apply (unfold Ifaces_def) 

385 
apply (simp (no_asm)) 

386 
done 

387 

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

389 
apply (unfold subint1_def Ifaces_def HasFooInt_def) 

390 
apply auto 

391 
done 

392 

393 
lemma unique_ifaces: "unique Ifaces" 

394 
apply (unfold Ifaces_def) 

395 
apply (simp (no_asm)) 

396 
done 

397 

398 
lemma unique_classes: "unique Classes" 

399 
apply (unfold table_classes_defs ) 

400 
apply (simp ) 

401 
done 

402 

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

404 
apply (rule SXcpt_subcls_Throwable_lemma) 

405 
apply auto 

406 
done 

407 

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

409 
apply (rule subcls_direct1) 

410 
apply (simp (no_asm) add: ExtCl_def) 

411 
apply (simp add: Object_def) 

412 
apply (simp (no_asm)) 

413 
done 

414 

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

416 
apply (rule subcls_direct2) 

417 
apply (simp (no_asm) add: ExtCl_def) 

418 
apply (simp add: Object_def) 

419 
apply (simp (no_asm)) 

420 
done 

421 

422 

423 

424 
section "fields and method lookup" 

425 

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

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

428 

429 
lemma fields_tprg_Throwable [simp]: 

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

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

432 

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

434 
apply (case_tac "xn = Throwable") 

435 
apply (simp (no_asm_simp)) 

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

437 

22708  438 
lemmas fields_rec' = fields_rec [OF _ ws_tprg] 
12854  439 

440 
lemma fields_Base [simp]: 

441 
"DeclConcepts.fields tprg Base 

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

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

22708  444 
apply (subst fields_rec') 
12854  445 
apply (auto simp add: BaseCl_def) 
446 
done 

447 

448 
lemma fields_Ext [simp]: 

449 
"DeclConcepts.fields tprg Ext 

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

451 
@ DeclConcepts.fields tprg Base" 

452 
apply (rule trans) 

22708  453 
apply (rule fields_rec') 
12854  454 
apply (auto simp add: ExtCl_def Object_def) 
455 
done 

456 

22708  457 
lemmas imethds_rec' = imethds_rec [OF _ ws_tprg] 
458 
lemmas methd_rec' = methd_rec [OF _ ws_tprg] 

12854  459 

460 
lemma imethds_HasFoo [simp]: 

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

462 
apply (rule trans) 

22708  463 
apply (rule imethds_rec') 
12854  464 
apply (auto simp add: HasFooInt_def) 
465 
done 

466 

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

22708  468 
apply (subst methd_rec') 
12854  469 
apply (auto simp add: Object_mdecls_def) 
470 
done 

471 

472 
lemma methd_Base [simp]: 

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

474 
apply (rule trans) 

22708  475 
apply (rule methd_rec') 
12854  476 
apply (auto simp add: BaseCl_def) 
477 
done 

478 

479 
lemma memberid_Base_foo_simp [simp]: 

480 
"memberid (mdecl Base_foo) = mid foo_sig" 

481 
by (simp add: Base_foo_def) 

482 

483 
lemma memberid_Ext_foo_simp [simp]: 

484 
"memberid (mdecl Ext_foo) = mid foo_sig" 

485 
by (simp add: Ext_foo_def) 

486 

487 
lemma Base_declares_foo: 

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

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

490 

491 
lemma foo_sig_not_undeclared_in_Base: 

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

493 
proof  

494 
from Base_declares_foo 

495 
show ?thesis 

496 
by (auto dest!: declared_not_undeclared ) 

497 
qed 

498 

499 
lemma Ext_declares_foo: 

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

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

502 

503 
lemma foo_sig_not_undeclared_in_Ext: 

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

505 
proof  

506 
from Ext_declares_foo 

507 
show ?thesis 

508 
by (auto dest!: declared_not_undeclared ) 

509 
qed 

510 

511 
lemma Base_foo_not_inherited_in_Ext: 

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

513 
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext) 

514 

515 
lemma Ext_method_inheritance: 

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

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

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

519 
= empty" 

520 
proof  

521 
from Base_foo_not_inherited_in_Ext 

522 
show ?thesis 

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

524 
qed 

525 

526 

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

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

529 
apply (rule trans) 

22708  530 
apply (rule methd_rec') 
12854  531 
apply (auto simp add: ExtCl_def Object_def Ext_method_inheritance) 
532 
done 

533 

534 
section "accessibility" 

535 

536 
lemma classesDefined: 

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

538 
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

539 
BaseCl_def ExtCl_def MainCl_def 
12854  540 
SXcptC_def ObjectC_def) 
541 
done 

542 

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

544 
proof  

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

546 
then show ?thesis 

547 
by (auto simp add: superclasses_rec BaseCl_def) 

548 
qed 

549 

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

551 
proof  

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

553 
then show ?thesis 

554 
by (auto simp add: superclasses_rec ExtCl_def BaseCl_def) 

555 
qed 

556 

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

557 
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

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

559 
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

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

561 
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

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

563 

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

566 

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

568 
by (simp add: is_acc_iface_def) 

569 

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

571 
by (simp add: is_acc_type_def) 

572 

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

574 
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def) 

575 

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

577 
by (simp add: is_acc_class_def) 

578 

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

580 
by (simp add: is_acc_type_def) 

581 

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

583 
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def) 

584 

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

586 
by (simp add: is_acc_class_def) 

587 

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

589 
by (simp add: is_acc_type_def) 

590 

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

592 
apply (unfold accmethd_def) 

593 
apply (simp) 

594 
done 

595 

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

597 
by (cases x) (auto) 

598 

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

600 
by (cases x) (auto) 

601 

602 
lemma foo_sig_undeclared_in_Object: 

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

604 
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def) 

605 

606 
lemma unique_sig_Base_foo: 

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

608 
by (auto simp add: declared_in_def cdeclaredmethd_def 

609 
Base_foo_def BaseCl_def) 

610 

611 
lemma Base_foo_no_override: 

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

613 
apply (drule overrides_commonD) 

614 
apply (clarsimp) 

615 
apply (frule subclsEval) 

616 
apply (rule ws_tprg) 

617 
apply (simp) 

618 
apply (rule classesDefined) 

619 
apply assumption+ 

620 
apply (frule unique_sig_Base_foo) 

621 
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object 

622 
dest: unique_sig_Base_foo) 

623 
done 

624 

625 
lemma Base_foo_no_stat_override: 

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

627 
apply (drule stat_overrides_commonD) 

628 
apply (clarsimp) 

629 
apply (frule subclsEval) 

630 
apply (rule ws_tprg) 

631 
apply (simp) 

632 
apply (rule classesDefined) 

633 
apply assumption+ 

634 
apply (frule unique_sig_Base_foo) 

635 
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object 

636 
dest: unique_sig_Base_foo) 

637 
done 

638 

639 

640 
lemma Base_foo_no_hide: 

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

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

643 

644 
lemma Ext_foo_no_hide: 

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

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

647 

648 
lemma unique_sig_Ext_foo: 

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

650 
by (auto simp add: declared_in_def cdeclaredmethd_def 

651 
Ext_foo_def ExtCl_def) 

652 

653 
lemma Ext_foo_override: 

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

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

656 
apply (drule overrides_commonD) 

657 
apply (clarsimp) 

658 
apply (frule subclsEval) 

659 
apply (rule ws_tprg) 

660 
apply (simp) 

661 
apply (rule classesDefined) 

662 
apply assumption+ 

663 
apply (frule unique_sig_Ext_foo) 

664 
apply (case_tac "old") 

665 
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 

666 
apply (auto simp add: ExtCl_def Ext_foo_def 

667 
BaseCl_def Base_foo_def Object_mdecls_def 

668 
split_paired_all 

669 
member_is_static_simp 

670 
dest: declared_not_undeclared unique_declaration) 

671 
done 

672 

673 
lemma Ext_foo_stat_override: 

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

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

676 
apply (drule stat_overrides_commonD) 

677 
apply (clarsimp) 

678 
apply (frule subclsEval) 

679 
apply (rule ws_tprg) 

680 
apply (simp) 

681 
apply (rule classesDefined) 

682 
apply assumption+ 

683 
apply (frule unique_sig_Ext_foo) 

684 
apply (case_tac "old") 

685 
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 

686 
apply (auto simp add: ExtCl_def Ext_foo_def 

687 
BaseCl_def Base_foo_def Object_mdecls_def 

688 
split_paired_all 

689 
member_is_static_simp 

690 
dest: declared_not_undeclared unique_declaration) 

691 
done 

692 

693 
lemma Base_foo_member_of_Base: 

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

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

696 

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

697 
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

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

699 
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

700 

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

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

704 

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

705 
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

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

707 
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

708 

12854  709 
lemma Base_foo_permits_acc: 
14030  710 
"tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S" 
12854  711 
by ( simp add: permits_acc_def Base_foo_def) 
712 

713 
lemma Base_foo_accessible [simp]: 

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

715 
by (auto intro: accessible_fromR.Immediate 
12854  716 
Base_foo_member_of_Base Base_foo_permits_acc) 
717 

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

718 
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

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

720 
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

721 
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

722 
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

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

724 

12854  725 
lemma accmethd_Base [simp]: 
726 
"accmethd tprg S Base = methd tprg Base" 

727 
apply (simp add: accmethd_def) 

728 
apply (rule filter_tab_all_True) 

729 
apply (simp add: snd_special_simp fst_special_simp) 

730 
done 

731 

732 
lemma Ext_foo_permits_acc: 

14030  733 
"tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S" 
12854  734 
by ( simp add: permits_acc_def Ext_foo_def) 
735 

736 
lemma Ext_foo_accessible [simp]: 

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

738 
by (auto intro: accessible_fromR.Immediate 
12854  739 
Ext_foo_member_of_Ext Ext_foo_permits_acc) 
740 

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

741 
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

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

743 
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

744 
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

745 
apply (rule Ext_foo_permits_acc) 
12854  746 
done 
747 

748 
lemma Ext_foo_overrides_Base_foo: 

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

750 
proof (rule overridesR.Direct, simp_all) 

751 
show "\<not> is_static Ext_foo" 

752 
by (simp add: member_is_static_simp Ext_foo_def) 

753 
show "\<not> is_static Base_foo" 

754 
by (simp add: member_is_static_simp Base_foo_def) 

755 
show "accmodi Ext_foo \<noteq> Private" 

756 
by (simp add: Ext_foo_def) 

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

758 
by (simp add: Ext_foo_def Base_foo_def) 

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

760 
by (auto intro: Ext_declares_foo) 

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

762 
by (auto intro: Base_declares_foo) 

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

764 
by (simp add: inheritable_in_def Base_foo_def) 

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

766 
by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp) 

767 
qed 

768 

769 
lemma accmethd_Ext [simp]: 

770 
"accmethd tprg S Ext = methd tprg Ext" 

771 
apply (simp add: accmethd_def) 

772 
apply (rule filter_tab_all_True) 

773 
apply (auto simp add: snd_special_simp fst_special_simp) 

774 
done 

775 

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

777 
by simp 

778 
lemma dynmethd_Ext_foo: 

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

780 
= Some (Ext,snd Ext_foo)" 

781 
proof  

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

783 
= Some (Base,snd Base_foo)" and 

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

785 
= Some (Ext,snd Ext_foo)" 

786 
by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def) 

787 
with cls_Ext ws_tprg Ext_foo_overrides_Base_foo 

788 
show ?thesis 

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

790 
qed 

791 

792 
lemma Base_fields_accessible[simp]: 

793 
"accfield tprg S Base 

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

795 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

796 
accessible_in_RefT_simp 

797 
is_public_def 

798 
BaseCl_def 

799 
permits_acc_def 

800 
declared_in_def 

801 
cdeclaredfield_def 

802 
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

803 
accessible_fromR.Immediate 
12854  804 
intro: members.Immediate) 
805 
done 

806 

807 

808 
lemma arr_member_of_Base: 

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

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

811 
member_of Base" 

812 
by (auto intro: members.Immediate 

813 
simp add: declared_in_def cdeclaredfield_def BaseCl_def) 

814 

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

815 
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

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

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

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

819 
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

820 

12854  821 
lemma arr_member_of_Ext: 
822 
"tprg\<turnstile>(Base, fdecl (arr, 

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

824 
member_of Ext" 

825 
apply (rule members.Inherited) 

826 
apply (simp add: inheritable_in_def) 

827 
apply (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def) 

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

829 
done 

830 

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

831 
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

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

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

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

835 
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

836 

12854  837 
lemma Ext_fields_accessible[simp]: 
838 
"accfield tprg S Ext 

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

840 
apply (auto simp add: accfield_def expand_fun_eq Let_def 

841 
accessible_in_RefT_simp 

842 
is_public_def 

843 
BaseCl_def 

844 
ExtCl_def 

845 
permits_acc_def 

846 
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

847 
accessible_fromR.Immediate) 
12854  848 
apply (auto intro: members.Immediate arr_member_of_Ext 
849 
simp add: declared_in_def cdeclaredfield_def ExtCl_def) 

850 
done 

851 

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

852 
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

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

854 
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

855 
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

856 
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

857 
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

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

859 

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

860 
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

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

862 
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

863 
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

864 
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

865 
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

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

867 

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

870 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

871 
done 

872 

873 
lemma PrimT_acc [simp]: 

874 
"is_acc_type tprg java_lang (PrimT t)" 

875 
apply (simp add: is_acc_type_def accessible_in_RefT_simp) 

876 
done 

877 

878 
lemma Object_acc [simp]: 

879 
"is_acc_class tprg java_lang Object" 

880 
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def) 

881 
done 

882 

883 

884 
section "wellformedness" 

885 

886 

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

888 
apply (unfold wf_idecl_def HasFooInt_def) 

889 
apply (auto intro!: wf_mheadI ws_idecl_HasFoo 

890 
simp add: foo_sig_def foo_mhead_def mhead_resTy_simp 

891 
member_is_static_simp ) 

892 
done 

893 

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

894 

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

895 
declare member_is_static_simp [simp] 
12854  896 
declare wt.Skip [rule del] wt.Init [rule del] 
24019  897 
ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *} 
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 
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

899 
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

900 

12854  901 
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def 
902 
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

903 

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

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

12854  906 

907 
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo" 

908 
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

909 
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
12854  910 
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

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

912 
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

913 
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

914 
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

915 
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

916 
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

917 
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

918 
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

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

921 
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

922 
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

923 
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

924 
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

925 
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

926 
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

927 
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

928 
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

929 
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

930 
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

931 
apply (simp) 
12854  932 
done 
933 

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

934 

12854  935 
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo" 
936 
apply (unfold Ext_foo_defs ) 

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

938 
simp add: mhead_resTy_simp ) 

939 
apply (rule wt.Cast) 

940 
prefer 2 

941 
apply simp 

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

943 
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

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

945 
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

946 
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

947 
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

948 
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

949 
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

950 
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

951 
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

952 
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

953 
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

954 
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

955 
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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
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

963 
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

964 
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

965 
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

966 
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

967 
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

968 
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

969 
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

970 
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

971 
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

972 
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

973 
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

974 
apply simp 
12854  975 
done 
976 

977 
declare mhead_resTy_simp [simp add] 

978 
declare member_is_static_simp [simp add] 

979 

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

981 
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def) 

982 
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

983 
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

984 
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

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

986 
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

987 
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

988 
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

989 
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

990 
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

991 
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

992 
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

993 
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

994 
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

995 
apply (rule da.Lit) 
12854  996 
apply (auto simp add: Base_foo_defs entails_def Let_def) 
997 
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

998 
apply (insert Base_foo_no_hide , simp add: Base_foo_def,blast) 
12854  999 
done 
1000 

1001 

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

1003 
apply (unfold wf_cdecl_def ExtCl_def) 

1004 
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

1005 
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

1006 
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

1007 
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

1008 
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

1009 
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

1010 
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

1011 
apply (insert Ext_foo_no_hide) 
12854  1012 
apply (simp_all add: qmdecl_def) 
1013 
apply blast+ 

1014 
done 

1015 

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

1016 
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

1017 
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

1018 
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

1019 
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

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

1021 

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

1024 
apply (simp (no_asm_simp)) 

1025 
apply (rule wf_HasFoo) 

1026 
done 

1027 

1028 
lemma wf_cdecl_all_standard_classes: 

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

1030 
apply (unfold standard_classes_def Let_def 

1031 
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) 

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

1033 
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

1034 
intro: da.Skip) 
12854  1035 
apply (auto simp add: Object_def Classes_def standard_classes_def 
1036 
SXcptC_def SXcpt_def) 

1037 
done 

1038 

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

1040 
apply (simp (no_asm) add: Classes_def) 

1041 
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

1042 
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

1043 
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

1044 
apply (rule wf_MainC [THEN conjI]) 
12854  1045 
apply (rule wf_cdecl_all_standard_classes) 
1046 
done 

1047 

1048 
theorem wf_tprg: "wf_prog tprg" 

1049 
apply (unfold wf_prog_def Let_def) 

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

1051 
apply (rule conjI) 

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

1053 
apply (rule conjI) 

1054 
apply (simp add: Object_mdecls_def) 

1055 
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

1056 
apply (cut_tac xn_cases) 
12854  1057 
apply (simp (no_asm_simp) add: Classes_def standard_classes_def) 
1058 
apply (insert wf_idecl_all) 

1059 
apply (insert wf_cdecl_all) 

1060 
apply auto 

1061 
done 

1062 

1063 
section "max spec" 

1064 

1065 
lemma appl_methds_Base_foo: 

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

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

1068 
,[Class Base])}" 

1069 
apply (unfold appl_methds_def) 

1070 
apply (simp (no_asm)) 

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

1072 
apply (auto simp add: cmheads_def Base_foo_defs) 

1073 
done 

1074 

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

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

1077 
, [Class Base])}" 

1078 
apply (unfold max_spec_def) 

1079 
apply (simp (no_asm) add: appl_methds_Base_foo) 

1080 
apply auto 

1081 
done 

1082 

1083 
section "welltypedness" 

1084 

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

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

1088 
apply (rule wtIs (* ;; *)) 

1089 
apply (rule wtIs (* Ass *)) 

1090 
apply (rule wtIs (* NewC *)) 

1091 
apply (rule wtIs (* LVar *)) 

1092 
apply (simp) 

1093 
apply (simp) 

1094 
apply (simp) 

1095 
apply (rule wtIs (* NewC *)) 

1096 
apply (simp) 

1097 
apply (simp) 

1098 
apply (rule wtIs (* Try *)) 

1099 
prefer 4 

1100 
apply (simp) 

1101 
defer 

1102 
apply (rule wtIs (* Expr *)) 

1103 
apply (rule wtIs (* Call *)) 

1104 
apply (rule wtIs (* Acc *)) 

1105 
apply (rule wtIs (* LVar *)) 

1106 
apply (simp) 

1107 
apply (simp) 

1108 
apply (rule wtIs (* Cons *)) 

1109 
apply (rule wtIs (* Lit *)) 

1110 
apply (simp) 

1111 
apply (rule wtIs (* Nil *)) 

1112 
apply (simp) 

1113 
apply (rule max_spec_Base_foo) 

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 (* While *)) 
1120 
apply (rule wtIs (* Acc *)) 

1121 
apply (rule wtIs (* AVar *)) 

1122 
apply (rule wtIs (* Acc *)) 

1123 
apply (rule wtIs (* FVar *)) 

1124 
apply (rule wtIs (* StatRef *)) 

1125 
apply (simp) 

1126 
apply (simp) 

1127 
apply (simp ) 

1128 
apply (simp) 

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

1129 
apply (simp) 
12854  1130 
apply (rule wtIs (* LVar *)) 
1131 
apply (simp) 

1132 
apply (rule wtIs (* Skip *)) 

1133 
done 

1134 

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

1135 
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

1136 

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

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

1139 
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

1140 
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

1141 
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

1142 
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

1143 
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

1144 
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

1145 
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

1146 
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

1147 
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

1148 
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

1149 
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

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

1152 
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

1153 
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

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

1156 
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

1157 
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

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

1160 
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

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

1163 
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

1164 
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

1165 
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

1166 
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

1167 
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

1168 
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

1169 
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

1170 
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

1171 
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

1172 
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

1173 
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

1174 
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

1175 
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

1176 
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

1177 

12854  1178 

1179 
section "execution" 

1180 

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

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

1183 
apply (frule atleast_free_SucD) 

1184 
apply (drule atleast_free_Suc [THEN iffD1]) 

1185 
apply clarsimp 

1186 
apply (frule new_Addr_SomeI) 

1187 
apply force 

1188 
done 

1189 

1190 
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp] 

1191 
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp] 

1192 
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] 

1193 
Base_foo_defs [simp] 

1194 

24019  1195 
ML_setup {* bind_thms ("eval_intros", map 
1196 
(simplify (simpset() delsimps @{thms Skip_eq} 

1197 
addsimps @{thms lvar_def}) o 

1198 
rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *} 

12854  1199 
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros 
1200 

1201 
consts 

1202 
a :: loc 

1203 
b :: loc 

1204 
c :: loc 

1205 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

1206 
abbreviation "one == Suc 0" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

1207 
abbreviation "two == Suc one" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

1208 
abbreviation "tree == Suc two" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20769
diff
changeset

1209 
abbreviation "four == Suc tree" 
12854  1210 

20769  1211 
syntax 
12854  1212 
obj_a :: obj 
1213 
obj_b :: obj 

1214 
obj_c :: obj 

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

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

1217 
globs1 :: globs 

1218 
globs2 :: globs 

1219 
globs3 :: globs 

1220 
globs8 :: globs 

1221 
locs3 :: locals 

1222 
locs4 :: locals 

1223 
locs8 :: locals 

1224 
s0 :: state 

1225 
s0' :: state 

1226 
s9' :: state 

1227 
s1 :: state 

1228 
s1' :: state 

1229 
s2 :: state 

1230 
s2' :: state 

1231 
s3 :: state 

1232 
s3' :: state 

1233 
s4 :: state 

1234 
s4' :: state 

1235 
s6' :: state 

1236 
s7' :: state 

1237 
s8 :: state 

1238 
s8' :: state 

1239 

1240 
translations 

20769  1241 
"obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) (CONST two) 
1242 
,values=CONST empty(Inr 0\<mapsto>Bool False)(Inr (CONST one)\<mapsto>Bool False)\<rparr>" 

1243 
"obj_b" <= "\<lparr>tag=CInst (CONST Ext) 

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

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

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

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

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

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

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

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

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

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

1254 
(Inl a\<mapsto>obj_a) 

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

12854  1256 
"globs3" == "globs2(Inl b\<mapsto>obj_b)" 
1257 
"globs8" == "globs3(Inl c\<mapsto>obj_c)" 

20769  1258 
"locs3" == "CONST empty(VName (CONST e)\<mapsto>Addr b)" 
1259 
"locs4" == "CONST empty(VName (CONST z)\<mapsto>Null)(Inr()\<mapsto>Addr b)" 

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

1261 
"s0" == " st (CONST empty) (CONST empty)" 

12854  1262 
"s0'" == " Norm s0" 
20769  1263 
"s1" == " st globs1 (CONST empty)" 
12854  1264 
"s1'" == " Norm s1" 
20769  1265 
"s2" == " st globs2 (CONST empty)" 
12854  1266 
"s2'" == " Norm s2" 
1267 
"s3" == " st globs3 locs3 " 

1268 
"s3'" == " Norm s3" 

1269 
"s4" == " st globs3 locs4" 

1270 
"s4'" == " Norm s4" 

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

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

1273 
"s8" == " st globs8 locs8" 

1274 
"s8'" == " Norm s8" 

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

1276 

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

00d4a435777f
Isabelle/Bali sources;
schi 