author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46714  a7ca72710dfe 
child 51717  9e7d1c139569 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Example.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Example Bali program *} 

5 

33965  6 
theory Example 
7 
imports Eval WellForm 

8 
begin 

12854  9 

10 
text {* 

11 
The following example Bali program includes: 

12 
\begin{itemize} 

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

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

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

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

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

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

19 
statement 

20 
\item instance creation and (default) static initialization 

21 
\end{itemize} 

22 
\begin{verbatim} 

23 
package java_lang 

24 

25 
public interface HasFoo { 

26 
public Base foo(Base z); 

27 
} 

28 

29 
public class Base implements HasFoo { 

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

31 
public HasFoo vee; 

32 
public Base foo(Base z) { 

33 
return z; 

34 
} 

35 
} 

36 

37 
public class Ext extends Base { 

38 
public int vee; 

39 
public Ext foo(Base z) { 

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

41 
return null; 

42 
} 

43 
} 

44 

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

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

48 
try {e.foo(null); } 

49 
catch(NullPointerException z) { 

50 
while(Ext.arr[2]) ; 

51 
} 

52 
} 

53 
} 

54 
\end{verbatim} 

55 
*} 

56 
declare widen.null [intro] 

57 

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

59 
apply (unfold wf_fdecl_def) 

60 
apply (simp (no_asm)) 

61 
done 

62 

63 
declare wf_fdecl_def2 [iff] 

64 

65 

66 
section "type and expression names" 

67 

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

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

71 
datatype label' = lab1' 

12854  72 

37956  73 
axiomatization 
74 
tnam' :: "tnam' \<Rightarrow> tnam" and 

75 
vnam' :: "vnam' \<Rightarrow> vname" and 

22708  76 
label':: "label' \<Rightarrow> label" 
37956  77 
where 
78 
(** tnam', vnam' and label are intended to be isomorphic 

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

37956  81 
inj_tnam' [simp]: "\<And>x y. (tnam' x = tnam' y) = (x = y)" and 
82 
inj_vnam' [simp]: "\<And>x y. (vnam' x = vnam' y) = (x = y)" and 

83 
inj_label' [simp]: "\<And>x y. (label' x = label' y) = (x = y)" and 

84 

85 
surj_tnam': "\<And>n. \<exists>m. n = tnam' m" and 

86 
surj_vnam': "\<And>n. \<exists>m. n = vnam' m" and 

87 
surj_label':" \<And>n. \<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 

37956  151 
axiomatization 
12854  152 
foo :: mname 
153 

37956  154 
definition 
155 
foo_sig :: sig 

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

12854  157 

37956  158 
definition 
159 
foo_mhead :: mhead 

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

12854  161 

37956  162 
definition 
163 
Base_foo :: mdecl 

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

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

166 

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

167 
definition Ext_foo :: mdecl 
37956  168 
where "Ext_foo = (foo_sig, 
12854  169 
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

170 
mbody=\<lparr>lcls=[] 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

171 
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

172 
Lit (Intg 1)) ;; 
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

173 
Return (Lit Null)\<rparr> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

174 
\<rparr>)" 
12854  175 

37956  176 
definition 
177 
arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" 

178 
where "arr_viewed_from accC C = {accC,Base,True}StatRef (ClassT C)..arr" 

12854  179 

37956  180 
definition 
181 
BaseCl :: "class" where 

182 
"BaseCl = \<lparr>access=Public, 

12854  183 
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

184 
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)], 
12854  185 
methods=[Base_foo], 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

186 
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

187 
:=New (PrimT Boolean)[Lit (Intg 2)]), 
12854  188 
super=Object, 
189 
superIfs=[HasFoo]\<rparr>" 

190 

37956  191 
definition 
192 
ExtCl :: "class" where 

193 
"ExtCl = \<lparr>access=Public, 

12854  194 
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
195 
methods=[Ext_foo], 

196 
init=Skip, 

197 
super=Base, 

198 
superIfs=[]\<rparr>" 

199 

37956  200 
definition 
201 
MainCl :: "class" where 

202 
"MainCl = \<lparr>access=Public, 

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

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

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

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

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

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

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

209 

37956  210 
definition 
211 
HasFooInt :: iface 

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

12854  213 

37956  214 
definition 
215 
Ifaces ::"idecl list" 

216 
where "Ifaces = [(HasFoo,HasFooInt)]" 

12854  217 

37956  218 
definition 
219 
"Classes" ::"cdecl list" 

220 
where "Classes = [(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 

28524  233 
,init=Skip,super=undefined,superIfs=[]\<rparr>" 
12854  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 

37956  275 
definition 
276 
test :: "(ty)list \<Rightarrow> stmt" where 

277 
"test pTs = (e:==NewC Ext;; 

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

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

461 
"imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))" 
12854  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))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

795 
apply (auto simp add: accfield_def fun_eq_iff Let_def 
12854  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))" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

840 
apply (auto simp add: accfield_def fun_eq_iff Let_def 
12854  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] 
26480  897 
ML {* 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 

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

980 
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def) 

981 
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

982 
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

983 
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

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

985 
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

986 
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

987 
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

988 
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

989 
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

990 
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

991 
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

992 
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

993 
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

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

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

1000 

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

1002 
apply (unfold wf_cdecl_def ExtCl_def) 

1003 
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

1004 
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

1005 
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

1006 
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

1007 
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

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 (insert Ext_foo_no_hide) 
12854  1011 
apply (simp_all add: qmdecl_def) 
1012 
apply blast+ 

1013 
done 

1014 

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

1015 
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

1016 
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

1017 
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

1018 
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

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

1020 

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

1023 
apply (simp (no_asm_simp)) 

1024 
apply (rule wf_HasFoo) 

1025 
done 

1026 

1027 
lemma wf_cdecl_all_standard_classes: 

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

1029 
apply (unfold standard_classes_def Let_def 

1030 
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) 

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

1032 
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

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

1036 
done 

1037 

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

1039 
apply (simp (no_asm) add: Classes_def) 

1040 
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

1041 
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

1042 
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

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

1046 

1047 
theorem wf_tprg: "wf_prog tprg" 

1048 
apply (unfold wf_prog_def Let_def) 

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

1050 
apply (rule conjI) 

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

1052 
apply (rule conjI) 

1053 
apply (simp add: Object_mdecls_def) 

1054 
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

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

1058 
apply (insert wf_cdecl_all) 

1059 
apply auto 

1060 
done 

1061 

1062 
section "max spec" 

1063 

1064 
lemma appl_methds_Base_foo: 

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

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

1067 
,[Class Base])}" 

1068 
apply (unfold appl_methds_def) 

1069 
apply (simp (no_asm)) 

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

1071 
apply (auto simp add: cmheads_def Base_foo_defs) 

1072 
done 

1073 

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

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

1076 
, [Class Base])}" 

31197
c1c163ec6c44
finetuned elimination of comprehensions involving x=t.
nipkow
parents:
31166
diff
changeset

1077 
by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if) 
12854  1078 

1079 
section "welltypedness" 

1080 

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

1084 
apply (rule wtIs (* ;; *)) 

1085 
apply (rule wtIs (* Ass *)) 

1086 
apply (rule wtIs (* NewC *)) 

1087 
apply (rule wtIs (* LVar *)) 

1088 
apply (simp) 

1089 
apply (simp) 

1090 
apply (simp) 

1091 
apply (rule wtIs (* NewC *)) 

1092 
apply (simp) 

1093 
apply (simp) 

1094 
apply (rule wtIs (* Try *)) 

1095 
prefer 4 

1096 
apply (simp) 

1097 
defer 

1098 
apply (rule wtIs (* Expr *)) 

1099 
apply (rule wtIs (* Call *)) 

1100 
apply (rule wtIs (* Acc *)) 

1101 
apply (rule wtIs (* LVar *)) 

1102 
apply (simp) 

1103 
apply (simp) 

1104 
apply (rule wtIs (* Cons *)) 

1105 
apply (rule wtIs (* Lit *)) 

1106 
apply (simp) 

1107 
apply (rule wtIs (* Nil *)) 

1108 
apply (simp) 

1109 
apply (rule max_spec_Base_foo) 

1110 
apply (simp) 

1111 
apply (simp) 

1112 
apply (simp) 

1113 
apply (simp) 

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

1114 
apply (simp) 
12854  1115 
apply (rule wtIs (* While *)) 
1116 
apply (rule wtIs (* Acc *)) 

1117 
apply (rule wtIs (* AVar *)) 

1118 
apply (rule wtIs (* Acc *)) 

1119 
apply (rule wtIs (* FVar *)) 

1120 
apply (rule wtIs (* StatRef *)) 

1121 
apply (simp) 

1122 
apply (simp) 

1123 
apply (simp ) 

1124 
apply (simp) 

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

1125 
apply (simp) 
12854  1126 
apply (rule wtIs (* LVar *)) 
1127 
apply (simp) 

1128 
apply (rule wtIs (* Skip *)) 

1129 
done 

1130 

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

1131 
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

1132 

36319  1133 
schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr> 
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

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

1135 
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

1136 
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

1137 
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

1138 
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

1139 
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

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

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

1142 
apply (rule da.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

1143 
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

1144 
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

1145 
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

1146 
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

1147 
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

1148 
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

1149 
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

1150 
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

1151 
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

1152 
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

1153 
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

1154 
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

1155 
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

1156 
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

1157 
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

1158 
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

1159 
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

1160 
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

1161 
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

1162 
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

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

1164 
apply (simp,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

1165 
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

1166 
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

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

1171 
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

1172 

12854  1173 

1174 
section "execution" 

1175 

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

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

1178 
apply (frule atleast_free_SucD) 

1179 
apply (drule atleast_free_Suc [THEN iffD1]) 

1180 
apply clarsimp 

1181 
apply (frule new_Addr_SomeI) 

1182 
apply force 

1183 
done 

1184 

1185 
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp] 

1186 
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp] 

1187 
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] 

1188 
Base_foo_defs [simp] 

1189 

26480  1190 
ML {* bind_thms ("eval_intros", map 
26342  1191 
(simplify (@{simpset} delsimps @{thms Skip_eq} 
24019  1192 
addsimps @{thms lvar_def}) o 
1193 
rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *} 

12854  1194 
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros 
1195 

37956  1196 
axiomatization 
1197 
a :: loc and 

1198 
b :: loc and 

12854  1199 
c :: loc 
1200 

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

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

1202 
abbreviation "two == Suc one" 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1203 
abbreviation "three == Suc two" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1204 
abbreviation "four == Suc three" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1205 

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

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

1207 
"obj_a == \<lparr>tag=Arr (PrimT Boolean) 2 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1208 
,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>" 
12854  1209 

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

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

1211 
"obj_b == \<lparr>tag=CInst Ext 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1212 
,values=(empty(Inl (vee, Base)\<mapsto>Null ) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1213 
(Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1214 

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

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

1216 
"obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1217 

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

1218 
abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1219 
abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1220 

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

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

1222 
"globs1 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1223 
(Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1224 
(Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)" 
12854  1225 

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

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

1227 
"globs2 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1228 
(Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1229 
(Inl a\<mapsto>obj_a) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1230 
(Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1231 

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

1232 
abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1233 
abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1234 
abbreviation "locs3 == empty(VName e\<mapsto>Addr b)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1235 
abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1236 

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

1237 
abbreviation "s0 == st empty empty" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1238 
abbreviation "s0' == Norm s0" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1239 
abbreviation "s1 == st globs1 empty" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1240 
abbreviation "s1' == Norm s1" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1241 
abbreviation "s2 == st globs2 empty" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1242 
abbreviation "s2' == Norm s2" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1243 
abbreviation "s3 == st globs3 locs3" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1244 
abbreviation "s3' == Norm s3" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1245 
abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1246 
abbreviation "s8 == st globs8 locs8" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1247 
abbreviation "s8' == Norm s8" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

1248 
abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)" 
12854  1249 

1250 

1251 
declare Pair_eq [simp del] 

36319  1252 
schematic_lemma exec_test: 
12854  1253 
"\<lbrakk>the (new_Addr (heap s1)) = a; 
1254 
the (new_Addr (heap ?s2)) = b; 

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

1256 
atleast_free (heap s0) four \<Longrightarrow> 

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

1258 
apply (unfold test_def arr_viewed_from_def) 

1259 
(* ?s9' = s9' *) 

1260 
apply (simp (no_asm_use)) 

1261 
apply (drule (1) alloc_one,clarsimp) 

1262 
apply (rule eval_Is (* ;; *)) 

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

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

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

1266 
apply (rule eval_Is (* Expr *)) 

1267 
apply (rule eval_Is (* Ass *)) 

1268 
apply (rule eval_Is (* LVar *)) 

1269 
apply (rule eval_Is (* NewC *)) 

1270 
(* begin init Ext *) 

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

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

1272 
apply (erule_tac V = "atleast_free ?h three" in thin_rl) 
12854  1273 
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl) 
1274 
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl) 

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

1276 
apply (simp) 

1277 
apply (rule conjI) 

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

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

1280 
apply (simp add: arr_viewed_from_def) 

1281 
apply (rule conjI) 

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

1283 
apply (simp) 

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

1285 
apply (rule HOL.refl) 

1286 
apply (simp) 

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

1288 
apply (rule eval_Is (* Expr *)) 

1289 
apply (rule eval_Is (* Ass *)) 

1290 
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

1291 
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

1292 
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

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

1294 
apply (simp add: check_field_access_def Let_def) 
12854  1295 
apply (rule eval_Is (* NewA *)) 
1296 
apply (simp) 

1297 
apply (rule eval_Is (* Lit *)) 

1298 
apply (simp) 

1299 
apply (rule halloc.New) 

1300 
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

1301 
apply (drule atleast_free_weaken,drule atleast_free_weaken) 
12854  1302 
apply (simp (no_asm_simp)) 
1303 
apply (simp add: upd_gobj_def) 

1304 
(* end init Ext *) 

1305 
apply (rule halloc.New) 

1306 
apply (drule alloc_one) 

1307 
prefer 2 apply fast 

1308 
apply (simp (no_asm_simp)) 

1309 
apply (drule atleast_free_weaken) 

1310 
apply force 

1311 
apply (simp) 

1312 
apply (drule alloc_one) 

1313 
apply (simp (no_asm_simp)) 

1314 
apply clarsimp 

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

1315 
apply (erule_tac V = "atleast_free ?h three" in thin_rl) 
12854  1316 
apply (drule_tac x = "a" in new_AddrD2 [THEN spec]) 
1317 
apply (simp (no_asm_use)) 

1318 
apply (rule eval_Is (* Try *)) 

1319 
apply (rule eval_Is (* Expr *)) 

1320 
(* begin method call *) 

1321 
apply (rule eval_Is (* Call *)) 

1322 
apply (rule eval_Is (* Acc *)) 

1323 
apply (rule eval_Is (* LVar *)) 

1324 
apply (rule eval_Is (* Cons *)) 

1325 
apply (rule eval_Is (* Lit *)) 

1326 
apply (rule eval_Is (* Nil *)) 

1327 
apply (simp) 

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

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

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

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

1331 
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

1332 
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

1333 
apply (rule Ext_foo_dyn_accessible) 
12854  1334 
apply (rule eval_Is (* Methd *)) 
1335 
apply (simp add: body_def Let_def) 

1336 
apply (rule eval_Is (* Body *)) 

1337 
apply (rule init_done, simp) 

1338 
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) 

1339 
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

1340 
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

1341 
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

1342 
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

1343 
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

1344 
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

1345 
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

1346 
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

1347 
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

1348 
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

1349 
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

1350 
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

1351 
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

1352 
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

1353 
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

1354 
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

1355 
apply (rule eval_Is (* Comp *)) 
12854  1356 
apply (simp) 
1357 
(* 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

1358 
apply simp 
12854  1359 
apply (rule sxalloc.intros) 
1360 
apply (rule halloc.New) 

1361 
apply (erule alloc_one [THEN conjunct1]) 

1362 
apply (simp (no_asm_simp)) 

1363 
apply (simp (no_asm_simp)) 

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

1365 
apply (drule alloc_one [THEN conjunct1]) 

1366 
apply (simp (no_asm_simp)) 

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

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

1369 
apply simp 

1370 
apply (rule eval_Is (* While *)) 

1371 
apply (rule eval_Is (* Acc *)) 

1372 
apply (rule eval_Is (* AVar *)) 

1373 
apply (rule eval_Is (* Acc *)) 

1374 
apply (rule eval_Is (* FVar *)) 

1375 
apply (rule init_done, simp) 
