12857
|
1 |
(* Title: HOL/Bali/Example.thy
|
12854
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
12858
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
12854
|
5 |
*)
|
|
6 |
header {* Example Bali program *}
|
|
7 |
|
|
8 |
theory Example = Eval + WellForm:
|
|
9 |
|
|
10 |
|
|
11 |
text {*
|
|
12 |
The following example Bali program includes:
|
|
13 |
\begin{itemize}
|
|
14 |
\item class and interface declarations with inheritance, hiding of fields,
|
|
15 |
overriding of methods (with refined result type), array type,
|
|
16 |
\item method call (with dynamic binding), parameter access, return expressions,
|
|
17 |
\item expression statements, sequential composition, literal values,
|
|
18 |
local assignment, local access, field assignment, type cast,
|
|
19 |
\item exception generation and propagation, try and catch statement, throw
|
|
20 |
statement
|
|
21 |
\item instance creation and (default) static initialization
|
|
22 |
\end{itemize}
|
|
23 |
\begin{verbatim}
|
|
24 |
package java_lang
|
|
25 |
|
|
26 |
public interface HasFoo {
|
|
27 |
public Base foo(Base z);
|
|
28 |
}
|
|
29 |
|
|
30 |
public class Base implements HasFoo {
|
|
31 |
static boolean arr[] = new boolean[2];
|
|
32 |
public HasFoo vee;
|
|
33 |
public Base foo(Base z) {
|
|
34 |
return z;
|
|
35 |
}
|
|
36 |
}
|
|
37 |
|
|
38 |
public class Ext extends Base {
|
|
39 |
public int vee;
|
|
40 |
public Ext foo(Base z) {
|
|
41 |
((Ext)z).vee = 1;
|
|
42 |
return null;
|
|
43 |
}
|
|
44 |
}
|
|
45 |
|
|
46 |
public class Example {
|
|
47 |
public static void main(String args[]) throws Throwable {
|
|
48 |
Base e = new Ext();
|
|
49 |
try {e.foo(null); }
|
|
50 |
catch(NullPointerException z) {
|
|
51 |
while(Ext.arr[2]) ;
|
|
52 |
}
|
|
53 |
}
|
|
54 |
}
|
|
55 |
\end{verbatim}
|
|
56 |
*}
|
|
57 |
|
|
58 |
declare widen.null [intro]
|
|
59 |
|
|
60 |
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
|
|
61 |
apply (unfold wf_fdecl_def)
|
|
62 |
apply (simp (no_asm))
|
|
63 |
done
|
|
64 |
|
|
65 |
declare wf_fdecl_def2 [iff]
|
|
66 |
|
|
67 |
|
|
68 |
section "type and expression names"
|
|
69 |
|
|
70 |
(** unfortunately cannot simply instantiate tnam **)
|
|
71 |
datatype tnam_ = HasFoo_ | Base_ | Ext_
|
|
72 |
datatype vnam_ = arr_ | vee_ | z_ | e_
|
|
73 |
datatype label_ = lab1_
|
|
74 |
|
|
75 |
consts
|
|
76 |
|
|
77 |
tnam_ :: "tnam_ \<Rightarrow> tnam"
|
|
78 |
vnam_ :: "vnam_ \<Rightarrow> vname"
|
|
79 |
label_:: "label_ \<Rightarrow> label"
|
|
80 |
axioms (** tnam_, vnam_ and label are intended to be isomorphic
|
|
81 |
to tnam, vname and label **)
|
|
82 |
|
|
83 |
inj_tnam_ [simp]: "(tnam_ x = tnam_ y) = (x = y)"
|
|
84 |
inj_vnam_ [simp]: "(vnam_ x = vnam_ y) = (x = y)"
|
|
85 |
inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
|
|
86 |
|
|
87 |
|
|
88 |
surj_tnam_: "\<exists>m. n = tnam_ m"
|
|
89 |
surj_vnam_: "\<exists>m. n = vnam_ m"
|
|
90 |
surj_label_:" \<exists>m. n = label_ m"
|
|
91 |
|
|
92 |
syntax
|
|
93 |
|
|
94 |
HasFoo :: qtname
|
|
95 |
Base :: qtname
|
|
96 |
Ext :: qtname
|
|
97 |
arr :: ename
|
|
98 |
vee :: ename
|
|
99 |
z :: ename
|
|
100 |
e :: ename
|
|
101 |
lab1:: label
|
|
102 |
translations
|
|
103 |
|
|
104 |
"HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
|
|
105 |
"Base" == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
|
|
106 |
"Ext" == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
|
|
107 |
"arr" == "(vnam_ arr_)"
|
|
108 |
"vee" == "(vnam_ vee_)"
|
|
109 |
"z" == "(vnam_ z_)"
|
|
110 |
"e" == "(vnam_ e_)"
|
|
111 |
"lab1" == "label_ lab1_"
|
|
112 |
|
|
113 |
|
|
114 |
lemma neq_Base_Object [simp]: "Base\<noteq>Object"
|
|
115 |
by (simp add: Object_def)
|
|
116 |
|
|
117 |
lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
|
|
118 |
by (simp add: Object_def)
|
|
119 |
|
|
120 |
lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
|
|
121 |
by (simp add: SXcpt_def)
|
|
122 |
|
|
123 |
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
|
|
124 |
by (simp add: SXcpt_def)
|
|
125 |
|
|
126 |
section "classes and interfaces"
|
|
127 |
|
|
128 |
defs
|
|
129 |
|
|
130 |
Object_mdecls_def: "Object_mdecls \<equiv> []"
|
|
131 |
SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []"
|
|
132 |
|
|
133 |
consts
|
|
134 |
|
|
135 |
foo :: mname
|
|
136 |
|
|
137 |
constdefs
|
|
138 |
|
|
139 |
foo_sig :: sig
|
|
140 |
"foo_sig \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
|
|
141 |
|
|
142 |
foo_mhead :: mhead
|
|
143 |
"foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
|
|
144 |
|
|
145 |
constdefs
|
|
146 |
|
|
147 |
Base_foo :: mdecl
|
|
148 |
"Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
|
|
149 |
mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
|
|
150 |
|
|
151 |
Ext_foo :: mdecl
|
|
152 |
"Ext_foo \<equiv> (foo_sig,
|
|
153 |
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
|
|
154 |
mbody=\<lparr>lcls=[]
|
|
155 |
,stmt=Expr({Ext,False}Cast (Class Ext) (!!z)..vee :=
|
|
156 |
Lit (Intg 1))\<rparr>
|
|
157 |
\<rparr>)"
|
|
158 |
|
|
159 |
constdefs
|
|
160 |
|
|
161 |
arr_viewed_from :: "qtname \<Rightarrow> var"
|
|
162 |
"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
|
|
163 |
|
|
164 |
BaseCl :: class
|
|
165 |
"BaseCl \<equiv> \<lparr>access=Public,
|
|
166 |
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
|
|
167 |
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)],
|
|
168 |
methods=[Base_foo],
|
|
169 |
init=Expr(arr_viewed_from Base :=New (PrimT Boolean)[Lit (Intg 2)]),
|
|
170 |
super=Object,
|
|
171 |
superIfs=[HasFoo]\<rparr>"
|
|
172 |
|
|
173 |
ExtCl :: class
|
|
174 |
"ExtCl \<equiv> \<lparr>access=Public,
|
|
175 |
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)],
|
|
176 |
methods=[Ext_foo],
|
|
177 |
init=Skip,
|
|
178 |
super=Base,
|
|
179 |
superIfs=[]\<rparr>"
|
|
180 |
|
|
181 |
constdefs
|
|
182 |
|
|
183 |
HasFooInt :: iface
|
|
184 |
"HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
|
|
185 |
|
|
186 |
Ifaces ::"idecl list"
|
|
187 |
"Ifaces \<equiv> [(HasFoo,HasFooInt)]"
|
|
188 |
|
|
189 |
"Classes" ::"cdecl list"
|
|
190 |
"Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
|
|
191 |
|
|
192 |
lemmas table_classes_defs =
|
|
193 |
Classes_def standard_classes_def ObjectC_def SXcptC_def
|
|
194 |
|
|
195 |
lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
|
|
196 |
apply (unfold Ifaces_def)
|
|
197 |
apply (simp (no_asm))
|
|
198 |
done
|
|
199 |
|
|
200 |
lemma table_classes_Object [simp]:
|
|
201 |
"table_of Classes Object = Some \<lparr>access=Public,cfields=[]
|
|
202 |
,methods=Object_mdecls
|
|
203 |
,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
|
|
204 |
apply (unfold table_classes_defs)
|
|
205 |
apply (simp (no_asm) add:Object_def)
|
|
206 |
done
|
|
207 |
|
|
208 |
lemma table_classes_SXcpt [simp]:
|
|
209 |
"table_of Classes (SXcpt xn)
|
|
210 |
= Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
|
|
211 |
init=Skip,
|
|
212 |
super=if xn = Throwable then Object else SXcpt Throwable,
|
|
213 |
superIfs=[]\<rparr>"
|
|
214 |
apply (unfold table_classes_defs)
|
|
215 |
apply (induct_tac xn)
|
|
216 |
apply (simp add: Object_def SXcpt_def)+
|
|
217 |
done
|
|
218 |
|
|
219 |
lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
|
|
220 |
apply (unfold table_classes_defs)
|
|
221 |
apply (simp (no_asm) add: Object_def SXcpt_def)
|
|
222 |
done
|
|
223 |
|
|
224 |
lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
|
|
225 |
apply (unfold table_classes_defs )
|
|
226 |
apply (simp (no_asm) add: Object_def SXcpt_def)
|
|
227 |
done
|
|
228 |
|
|
229 |
lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
|
|
230 |
apply (unfold table_classes_defs )
|
|
231 |
apply (simp (no_asm) add: Object_def SXcpt_def)
|
|
232 |
done
|
|
233 |
|
|
234 |
|
|
235 |
section "program"
|
|
236 |
|
|
237 |
syntax
|
|
238 |
tprg :: prog
|
|
239 |
|
|
240 |
translations
|
|
241 |
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
|
|
242 |
|
|
243 |
constdefs
|
|
244 |
test :: "(ty)list \<Rightarrow> stmt"
|
|
245 |
"test pTs \<equiv> e:==NewC Ext;;
|
|
246 |
\<spacespace> Try Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
|
|
247 |
\<spacespace> Catch((SXcpt NullPointer) z)
|
|
248 |
(lab1\<bullet> While(Acc (Acc (arr_viewed_from Ext).[Lit (Intg 2)])) Skip)"
|
|
249 |
|
|
250 |
|
|
251 |
section "well-structuredness"
|
|
252 |
|
|
253 |
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
|
|
254 |
apply (auto dest!: tranclD subcls1D)
|
|
255 |
done
|
|
256 |
|
|
257 |
lemma not_Throwable_subcls_SXcpt [elim!]:
|
|
258 |
"(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
|
|
259 |
apply (auto dest!: tranclD subcls1D)
|
|
260 |
apply (simp add: Object_def SXcpt_def)
|
|
261 |
done
|
|
262 |
|
|
263 |
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]:
|
|
264 |
"(SXcpt xn, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
|
|
265 |
apply (auto dest!: tranclD subcls1D)
|
|
266 |
apply (drule rtranclD)
|
|
267 |
apply auto
|
|
268 |
done
|
|
269 |
|
|
270 |
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
|
|
271 |
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
|
|
272 |
done
|
|
273 |
|
|
274 |
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]:
|
|
275 |
"(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>)
|
|
276 |
\<in> (subcls1 tprg)^+ \<longrightarrow> R"
|
|
277 |
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
|
|
278 |
apply (erule ssubst)
|
|
279 |
apply (rule tnam_.induct)
|
|
280 |
apply safe
|
|
281 |
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def)
|
|
282 |
apply (drule rtranclD)
|
|
283 |
apply auto
|
|
284 |
done
|
|
285 |
|
|
286 |
|
|
287 |
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
|
|
288 |
apply (unfold ws_idecl_def)
|
|
289 |
apply (simp (no_asm))
|
|
290 |
done
|
|
291 |
|
|
292 |
lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
|
|
293 |
apply (unfold ws_cdecl_def)
|
|
294 |
apply auto
|
|
295 |
done
|
|
296 |
|
|
297 |
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
|
|
298 |
apply (unfold ws_cdecl_def)
|
|
299 |
apply auto
|
|
300 |
done
|
|
301 |
|
|
302 |
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
|
|
303 |
apply (unfold ws_cdecl_def)
|
|
304 |
apply auto
|
|
305 |
done
|
|
306 |
|
|
307 |
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
|
|
308 |
apply (unfold ws_cdecl_def)
|
|
309 |
apply auto
|
|
310 |
done
|
|
311 |
|
|
312 |
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
|
|
313 |
apply (unfold ws_cdecl_def)
|
|
314 |
apply auto
|
|
315 |
done
|
|
316 |
|
|
317 |
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
|
|
318 |
ws_cdecl_Base ws_cdecl_Ext
|
|
319 |
|
|
320 |
declare not_Object_subcls_any [rule del]
|
|
321 |
not_Throwable_subcls_SXcpt [rule del]
|
|
322 |
not_SXcpt_n_subcls_SXcpt_n [rule del]
|
|
323 |
not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
|
|
324 |
|
|
325 |
lemma ws_idecl_all:
|
|
326 |
"G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
|
|
327 |
apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
|
|
328 |
apply (auto intro!: ws_idecl_HasFoo)
|
|
329 |
done
|
|
330 |
|
|
331 |
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
|
|
332 |
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def)
|
|
333 |
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def
|
|
334 |
SXcptC_def)
|
|
335 |
done
|
|
336 |
|
|
337 |
lemma ws_tprg: "ws_prog tprg"
|
|
338 |
apply (unfold ws_prog_def)
|
|
339 |
apply (auto intro!: ws_idecl_all ws_cdecl_all)
|
|
340 |
done
|
|
341 |
|
|
342 |
|
|
343 |
section "misc program properties (independent of well-structuredness)"
|
|
344 |
|
|
345 |
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
|
|
346 |
apply (unfold Ifaces_def)
|
|
347 |
apply (simp (no_asm))
|
|
348 |
done
|
|
349 |
|
|
350 |
lemma empty_subint1 [simp]: "subint1 tprg = {}"
|
|
351 |
apply (unfold subint1_def Ifaces_def HasFooInt_def)
|
|
352 |
apply auto
|
|
353 |
done
|
|
354 |
|
|
355 |
lemma unique_ifaces: "unique Ifaces"
|
|
356 |
apply (unfold Ifaces_def)
|
|
357 |
apply (simp (no_asm))
|
|
358 |
done
|
|
359 |
|
|
360 |
lemma unique_classes: "unique Classes"
|
|
361 |
apply (unfold table_classes_defs )
|
|
362 |
apply (simp )
|
|
363 |
done
|
|
364 |
|
|
365 |
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
|
|
366 |
apply (rule SXcpt_subcls_Throwable_lemma)
|
|
367 |
apply auto
|
|
368 |
done
|
|
369 |
|
|
370 |
lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
|
|
371 |
apply (rule subcls_direct1)
|
|
372 |
apply (simp (no_asm) add: ExtCl_def)
|
|
373 |
apply (simp add: Object_def)
|
|
374 |
apply (simp (no_asm))
|
|
375 |
done
|
|
376 |
|
|
377 |
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
|
|
378 |
apply (rule subcls_direct2)
|
|
379 |
apply (simp (no_asm) add: ExtCl_def)
|
|
380 |
apply (simp add: Object_def)
|
|
381 |
apply (simp (no_asm))
|
|
382 |
done
|
|
383 |
|
|
384 |
|
|
385 |
|
|
386 |
section "fields and method lookup"
|
|
387 |
|
|
388 |
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
|
|
389 |
by (rule ws_tprg [THEN fields_emptyI], force+)
|
|
390 |
|
|
391 |
lemma fields_tprg_Throwable [simp]:
|
|
392 |
"DeclConcepts.fields tprg (SXcpt Throwable) = []"
|
|
393 |
by (rule ws_tprg [THEN fields_emptyI], force+)
|
|
394 |
|
|
395 |
lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
|
|
396 |
apply (case_tac "xn = Throwable")
|
|
397 |
apply (simp (no_asm_simp))
|
|
398 |
by (rule ws_tprg [THEN fields_emptyI], force+)
|
|
399 |
|
|
400 |
lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
|
|
401 |
|
|
402 |
lemma fields_Base [simp]:
|
|
403 |
"DeclConcepts.fields tprg Base
|
|
404 |
= [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
|
|
405 |
((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)]"
|
|
406 |
apply (subst fields_rec_)
|
|
407 |
apply (auto simp add: BaseCl_def)
|
|
408 |
done
|
|
409 |
|
|
410 |
lemma fields_Ext [simp]:
|
|
411 |
"DeclConcepts.fields tprg Ext
|
|
412 |
= [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)]
|
|
413 |
@ DeclConcepts.fields tprg Base"
|
|
414 |
apply (rule trans)
|
|
415 |
apply (rule fields_rec_)
|
|
416 |
apply (auto simp add: ExtCl_def Object_def)
|
|
417 |
done
|
|
418 |
|
|
419 |
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
|
|
420 |
lemmas methd_rec_ = methd_rec [OF _ ws_tprg]
|
|
421 |
|
|
422 |
lemma imethds_HasFoo [simp]:
|
|
423 |
"imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
|
|
424 |
apply (rule trans)
|
|
425 |
apply (rule imethds_rec_)
|
|
426 |
apply (auto simp add: HasFooInt_def)
|
|
427 |
done
|
|
428 |
|
|
429 |
lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
|
|
430 |
apply (subst methd_rec_)
|
|
431 |
apply (auto simp add: Object_mdecls_def)
|
|
432 |
done
|
|
433 |
|
|
434 |
lemma methd_Base [simp]:
|
|
435 |
"methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
|
|
436 |
apply (rule trans)
|
|
437 |
apply (rule methd_rec_)
|
|
438 |
apply (auto simp add: BaseCl_def)
|
|
439 |
done
|
|
440 |
|
|
441 |
(* ### To Table *)
|
|
442 |
lemma filter_tab_all_False:
|
|
443 |
"\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
|
|
444 |
by (auto simp add: filter_tab_def expand_fun_eq)
|
|
445 |
|
|
446 |
|
|
447 |
lemma memberid_Base_foo_simp [simp]:
|
|
448 |
"memberid (mdecl Base_foo) = mid foo_sig"
|
|
449 |
by (simp add: Base_foo_def)
|
|
450 |
|
|
451 |
lemma memberid_Ext_foo_simp [simp]:
|
|
452 |
"memberid (mdecl Ext_foo) = mid foo_sig"
|
|
453 |
by (simp add: Ext_foo_def)
|
|
454 |
|
|
455 |
lemma Base_declares_foo:
|
|
456 |
"tprg\<turnstile>mdecl Base_foo declared_in Base"
|
|
457 |
by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
|
|
458 |
|
|
459 |
lemma foo_sig_not_undeclared_in_Base:
|
|
460 |
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
|
|
461 |
proof -
|
|
462 |
from Base_declares_foo
|
|
463 |
show ?thesis
|
|
464 |
by (auto dest!: declared_not_undeclared )
|
|
465 |
qed
|
|
466 |
|
|
467 |
lemma Ext_declares_foo:
|
|
468 |
"tprg\<turnstile>mdecl Ext_foo declared_in Ext"
|
|
469 |
by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
|
|
470 |
|
|
471 |
lemma foo_sig_not_undeclared_in_Ext:
|
|
472 |
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
|
|
473 |
proof -
|
|
474 |
from Ext_declares_foo
|
|
475 |
show ?thesis
|
|
476 |
by (auto dest!: declared_not_undeclared )
|
|
477 |
qed
|
|
478 |
|
|
479 |
lemma Base_foo_not_inherited_in_Ext:
|
|
480 |
"\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
|
|
481 |
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
|
|
482 |
|
|
483 |
lemma Ext_method_inheritance:
|
|
484 |
"filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
|
|
485 |
(empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
|
|
486 |
snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
|
|
487 |
= empty"
|
|
488 |
proof -
|
|
489 |
from Base_foo_not_inherited_in_Ext
|
|
490 |
show ?thesis
|
|
491 |
by (auto intro: filter_tab_all_False simp add: Base_foo_def)
|
|
492 |
qed
|
|
493 |
|
|
494 |
|
|
495 |
lemma methd_Ext [simp]: "methd tprg Ext =
|
|
496 |
table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
|
|
497 |
apply (rule trans)
|
|
498 |
apply (rule methd_rec_)
|
|
499 |
apply (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
|
|
500 |
done
|
|
501 |
|
|
502 |
section "accessibility"
|
|
503 |
|
|
504 |
lemma classesDefined:
|
|
505 |
"\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
|
|
506 |
apply (auto simp add: Classes_def standard_classes_def
|
|
507 |
BaseCl_def ExtCl_def
|
|
508 |
SXcptC_def ObjectC_def)
|
|
509 |
done
|
|
510 |
|
|
511 |
lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
|
|
512 |
proof -
|
|
513 |
have ws: "ws_prog tprg" by (rule ws_tprg)
|
|
514 |
then show ?thesis
|
|
515 |
by (auto simp add: superclasses_rec BaseCl_def)
|
|
516 |
qed
|
|
517 |
|
|
518 |
lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
|
|
519 |
proof -
|
|
520 |
have ws: "ws_prog tprg" by (rule ws_tprg)
|
|
521 |
then show ?thesis
|
|
522 |
by (auto simp add: superclasses_rec ExtCl_def BaseCl_def)
|
|
523 |
qed
|
|
524 |
|
|
525 |
lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P"
|
|
526 |
by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
|
|
527 |
|
|
528 |
lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
|
|
529 |
by (simp add: is_acc_iface_def)
|
|
530 |
|
|
531 |
lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
|
|
532 |
by (simp add: is_acc_type_def)
|
|
533 |
|
|
534 |
lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P"
|
|
535 |
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
|
|
536 |
|
|
537 |
lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
|
|
538 |
by (simp add: is_acc_class_def)
|
|
539 |
|
|
540 |
lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
|
|
541 |
by (simp add: is_acc_type_def)
|
|
542 |
|
|
543 |
lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P"
|
|
544 |
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
|
|
545 |
|
|
546 |
lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
|
|
547 |
by (simp add: is_acc_class_def)
|
|
548 |
|
|
549 |
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
|
|
550 |
by (simp add: is_acc_type_def)
|
|
551 |
|
|
552 |
lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
|
|
553 |
apply (unfold accmethd_def)
|
|
554 |
apply (simp)
|
|
555 |
done
|
|
556 |
|
|
557 |
lemma snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
|
|
558 |
by (cases x) (auto)
|
|
559 |
|
|
560 |
lemma fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
|
|
561 |
by (cases x) (auto)
|
|
562 |
|
|
563 |
lemma foo_sig_undeclared_in_Object:
|
|
564 |
"tprg\<turnstile>mid foo_sig undeclared_in Object"
|
|
565 |
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
|
|
566 |
|
|
567 |
(* ### To DeclConcepts *)
|
|
568 |
lemma undeclared_not_declared:
|
|
569 |
"G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C"
|
|
570 |
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
|
|
571 |
|
|
572 |
|
|
573 |
lemma unique_sig_Base_foo:
|
|
574 |
"tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
|
|
575 |
by (auto simp add: declared_in_def cdeclaredmethd_def
|
|
576 |
Base_foo_def BaseCl_def)
|
|
577 |
|
|
578 |
lemma Base_foo_no_override:
|
|
579 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
|
|
580 |
apply (drule overrides_commonD)
|
|
581 |
apply (clarsimp)
|
|
582 |
apply (frule subclsEval)
|
|
583 |
apply (rule ws_tprg)
|
|
584 |
apply (simp)
|
|
585 |
apply (rule classesDefined)
|
|
586 |
apply assumption+
|
|
587 |
apply (frule unique_sig_Base_foo)
|
|
588 |
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
|
|
589 |
dest: unique_sig_Base_foo)
|
|
590 |
done
|
|
591 |
|
|
592 |
lemma Base_foo_no_stat_override:
|
|
593 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
|
|
594 |
apply (drule stat_overrides_commonD)
|
|
595 |
apply (clarsimp)
|
|
596 |
apply (frule subclsEval)
|
|
597 |
apply (rule ws_tprg)
|
|
598 |
apply (simp)
|
|
599 |
apply (rule classesDefined)
|
|
600 |
apply assumption+
|
|
601 |
apply (frule unique_sig_Base_foo)
|
|
602 |
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
|
|
603 |
dest: unique_sig_Base_foo)
|
|
604 |
done
|
|
605 |
|
|
606 |
|
|
607 |
lemma Base_foo_no_hide:
|
|
608 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
|
|
609 |
by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
|
|
610 |
|
|
611 |
lemma Ext_foo_no_hide:
|
|
612 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
|
|
613 |
by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
|
|
614 |
|
|
615 |
lemma unique_sig_Ext_foo:
|
|
616 |
"tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
|
|
617 |
by (auto simp add: declared_in_def cdeclaredmethd_def
|
|
618 |
Ext_foo_def ExtCl_def)
|
|
619 |
|
|
620 |
(* ### To DeclConcepts *)
|
|
621 |
lemma unique_declaration:
|
|
622 |
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk>
|
|
623 |
\<Longrightarrow> m = n"
|
|
624 |
apply (cases m)
|
|
625 |
apply (cases n,
|
|
626 |
auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
|
|
627 |
done
|
|
628 |
|
|
629 |
|
|
630 |
lemma Ext_foo_override:
|
|
631 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old
|
|
632 |
\<Longrightarrow> old = (Base,(snd Base_foo))"
|
|
633 |
apply (drule overrides_commonD)
|
|
634 |
apply (clarsimp)
|
|
635 |
apply (frule subclsEval)
|
|
636 |
apply (rule ws_tprg)
|
|
637 |
apply (simp)
|
|
638 |
apply (rule classesDefined)
|
|
639 |
apply assumption+
|
|
640 |
apply (frule unique_sig_Ext_foo)
|
|
641 |
apply (case_tac "old")
|
|
642 |
apply (insert Base_declares_foo foo_sig_undeclared_in_Object)
|
|
643 |
apply (auto simp add: ExtCl_def Ext_foo_def
|
|
644 |
BaseCl_def Base_foo_def Object_mdecls_def
|
|
645 |
split_paired_all
|
|
646 |
member_is_static_simp
|
|
647 |
dest: declared_not_undeclared unique_declaration)
|
|
648 |
done
|
|
649 |
|
|
650 |
lemma Ext_foo_stat_override:
|
|
651 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old
|
|
652 |
\<Longrightarrow> old = (Base,(snd Base_foo))"
|
|
653 |
apply (drule stat_overrides_commonD)
|
|
654 |
apply (clarsimp)
|
|
655 |
apply (frule subclsEval)
|
|
656 |
apply (rule ws_tprg)
|
|
657 |
apply (simp)
|
|
658 |
apply (rule classesDefined)
|
|
659 |
apply assumption+
|
|
660 |
apply (frule unique_sig_Ext_foo)
|
|
661 |
apply (case_tac "old")
|
|
662 |
apply (insert Base_declares_foo foo_sig_undeclared_in_Object)
|
|
663 |
apply (auto simp add: ExtCl_def Ext_foo_def
|
|
664 |
BaseCl_def Base_foo_def Object_mdecls_def
|
|
665 |
split_paired_all
|
|
666 |
member_is_static_simp
|
|
667 |
dest: declared_not_undeclared unique_declaration)
|
|
668 |
done
|
|
669 |
|
|
670 |
(*### weiter hoch *)
|
|
671 |
lemma Base_foo_member_of_Base:
|
|
672 |
"tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
|
|
673 |
by (auto intro!: members.Immediate Base_declares_foo)
|
|
674 |
|
|
675 |
(*### weiter hoch *)
|
|
676 |
lemma Ext_foo_member_of_Ext:
|
|
677 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
|
|
678 |
by (auto intro!: members.Immediate Ext_declares_foo)
|
|
679 |
|
|
680 |
lemma Base_foo_permits_acc:
|
|
681 |
"tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
|
|
682 |
by ( simp add: permits_acc_def Base_foo_def)
|
|
683 |
|
|
684 |
lemma Base_foo_accessible [simp]:
|
|
685 |
"tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
|
|
686 |
by (auto intro: accessible_fromR.immediate
|
|
687 |
Base_foo_member_of_Base Base_foo_permits_acc)
|
|
688 |
|
|
689 |
lemma accmethd_Base [simp]:
|
|
690 |
"accmethd tprg S Base = methd tprg Base"
|
|
691 |
apply (simp add: accmethd_def)
|
|
692 |
apply (rule filter_tab_all_True)
|
|
693 |
apply (simp add: snd_special_simp fst_special_simp)
|
|
694 |
done
|
|
695 |
|
|
696 |
lemma Ext_foo_permits_acc:
|
|
697 |
"tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
|
|
698 |
by ( simp add: permits_acc_def Ext_foo_def)
|
|
699 |
|
|
700 |
lemma Ext_foo_accessible [simp]:
|
|
701 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
|
|
702 |
by (auto intro: accessible_fromR.immediate
|
|
703 |
Ext_foo_member_of_Ext Ext_foo_permits_acc)
|
|
704 |
|
|
705 |
(*
|
|
706 |
lemma Base_foo_accessible_through_inheritance_in_Ext [simp]:
|
|
707 |
"tprg\<turnstile>(Base,snd Base_foo) accessible_through_inheritance_in Ext"
|
|
708 |
apply (rule accessible_through_inheritance.Direct)
|
|
709 |
apply simp
|
|
710 |
apply (simp add: accessible_for_inheritance_in_def Base_foo_def)
|
|
711 |
done
|
|
712 |
*)
|
|
713 |
|
|
714 |
lemma Ext_foo_overrides_Base_foo:
|
|
715 |
"tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
|
|
716 |
proof (rule overridesR.Direct, simp_all)
|
|
717 |
show "\<not> is_static Ext_foo"
|
|
718 |
by (simp add: member_is_static_simp Ext_foo_def)
|
|
719 |
show "\<not> is_static Base_foo"
|
|
720 |
by (simp add: member_is_static_simp Base_foo_def)
|
|
721 |
show "accmodi Ext_foo \<noteq> Private"
|
|
722 |
by (simp add: Ext_foo_def)
|
|
723 |
show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
|
|
724 |
by (simp add: Ext_foo_def Base_foo_def)
|
|
725 |
show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
|
|
726 |
by (auto intro: Ext_declares_foo)
|
|
727 |
show "tprg\<turnstile>mdecl Base_foo declared_in Base"
|
|
728 |
by (auto intro: Base_declares_foo)
|
|
729 |
show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
|
|
730 |
by (simp add: inheritable_in_def Base_foo_def)
|
|
731 |
show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
|
|
732 |
by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
|
|
733 |
qed
|
|
734 |
|
|
735 |
(*
|
|
736 |
lemma Base_foo_of_Ext_accessible[simp]:
|
|
737 |
"tprg\<turnstile>(Base, mdecl Base_foo) of Ext accessible_from S"
|
|
738 |
apply (auto intro: accessible_fromR.immediate
|
|
739 |
Base_foo_member_of_Base Base_foo_permits_acc)
|
|
740 |
apply (rule accessible_fromR.immediate)
|
|
741 |
apply (rule_tac "old"="(Base,Base_foo)" and sup="Base"
|
|
742 |
in accessible_fromR.overriding)
|
|
743 |
apply (auto intro!: Ext_foo_overrides_Base_foo)
|
|
744 |
apply (auto
|
|
745 |
apply (insert Ext_foo_overrides_Base_foo)
|
|
746 |
apply (rule accessible_fromR.overriding, simp_all)
|
|
747 |
apply (auto intro!: Ext_foo_overrides_Base_foo)
|
|
748 |
apply (auto intro!: accessible_fromR.overriding
|
|
749 |
intro: Ext_foo_overrides_Base_foo)
|
|
750 |
by
|
|
751 |
Ext_foo_member_of_Ext Ext_foo_permits_acc)
|
|
752 |
apply (auto intro!: accessible
|
|
753 |
apply (auto simp add: method_accessible_from_def accessible_from_def)
|
|
754 |
apply (simp add: Base_foo_def)
|
|
755 |
done
|
|
756 |
*)
|
|
757 |
|
|
758 |
lemma accmethd_Ext [simp]:
|
|
759 |
"accmethd tprg S Ext = methd tprg Ext"
|
|
760 |
apply (simp add: accmethd_def)
|
|
761 |
apply (rule filter_tab_all_True)
|
|
762 |
apply (auto simp add: snd_special_simp fst_special_simp)
|
|
763 |
done
|
|
764 |
|
|
765 |
(* ### Weiter hoch *)
|
|
766 |
lemma cls_Ext: "class tprg Ext = Some ExtCl"
|
|
767 |
by simp
|
|
768 |
lemma dynmethd_Ext_foo:
|
|
769 |
"dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr>
|
|
770 |
= Some (Ext,snd Ext_foo)"
|
|
771 |
proof -
|
|
772 |
have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr>
|
|
773 |
= Some (Base,snd Base_foo)" and
|
|
774 |
"methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr>
|
|
775 |
= Some (Ext,snd Ext_foo)"
|
|
776 |
by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
|
|
777 |
with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
|
|
778 |
show ?thesis
|
|
779 |
by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
|
|
780 |
qed
|
|
781 |
|
|
782 |
lemma Base_fields_accessible[simp]:
|
|
783 |
"accfield tprg S Base
|
|
784 |
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
|
|
785 |
apply (auto simp add: accfield_def expand_fun_eq Let_def
|
|
786 |
accessible_in_RefT_simp
|
|
787 |
is_public_def
|
|
788 |
BaseCl_def
|
|
789 |
permits_acc_def
|
|
790 |
declared_in_def
|
|
791 |
cdeclaredfield_def
|
|
792 |
intro!: filter_tab_all_True_Some filter_tab_None
|
|
793 |
accessible_fromR.immediate
|
|
794 |
intro: members.Immediate)
|
|
795 |
done
|
|
796 |
|
|
797 |
|
|
798 |
lemma arr_member_of_Base:
|
|
799 |
"tprg\<turnstile>(Base, fdecl (arr,
|
|
800 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
|
|
801 |
member_of Base"
|
|
802 |
by (auto intro: members.Immediate
|
|
803 |
simp add: declared_in_def cdeclaredfield_def BaseCl_def)
|
|
804 |
|
|
805 |
lemma arr_member_of_Ext:
|
|
806 |
"tprg\<turnstile>(Base, fdecl (arr,
|
|
807 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
|
|
808 |
member_of Ext"
|
|
809 |
apply (rule members.Inherited)
|
|
810 |
apply (simp add: inheritable_in_def)
|
|
811 |
apply (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
|
|
812 |
apply (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
|
|
813 |
done
|
|
814 |
|
|
815 |
lemma Ext_fields_accessible[simp]:
|
|
816 |
"accfield tprg S Ext
|
|
817 |
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
|
|
818 |
apply (auto simp add: accfield_def expand_fun_eq Let_def
|
|
819 |
accessible_in_RefT_simp
|
|
820 |
is_public_def
|
|
821 |
BaseCl_def
|
|
822 |
ExtCl_def
|
|
823 |
permits_acc_def
|
|
824 |
intro!: filter_tab_all_True_Some filter_tab_None
|
|
825 |
accessible_fromR.immediate)
|
|
826 |
apply (auto intro: members.Immediate arr_member_of_Ext
|
|
827 |
simp add: declared_in_def cdeclaredfield_def ExtCl_def)
|
|
828 |
done
|
|
829 |
|
|
830 |
lemma array_of_PrimT_acc [simp]:
|
|
831 |
"is_acc_type tprg java_lang (PrimT t.[])"
|
|
832 |
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
|
|
833 |
done
|
|
834 |
|
|
835 |
lemma PrimT_acc [simp]:
|
|
836 |
"is_acc_type tprg java_lang (PrimT t)"
|
|
837 |
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
|
|
838 |
done
|
|
839 |
|
|
840 |
lemma Object_acc [simp]:
|
|
841 |
"is_acc_class tprg java_lang Object"
|
|
842 |
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
|
|
843 |
done
|
|
844 |
|
|
845 |
|
|
846 |
section "well-formedness"
|
|
847 |
|
|
848 |
|
|
849 |
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
|
|
850 |
apply (unfold wf_idecl_def HasFooInt_def)
|
|
851 |
apply (auto intro!: wf_mheadI ws_idecl_HasFoo
|
|
852 |
simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
|
|
853 |
member_is_static_simp )
|
|
854 |
done
|
|
855 |
|
|
856 |
declare wt.Skip [rule del] wt.Init [rule del]
|
|
857 |
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
|
|
858 |
lemmas Ext_foo_defs = Ext_foo_def foo_sig_def
|
|
859 |
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
|
|
860 |
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
|
|
861 |
|
|
862 |
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
|
|
863 |
apply (unfold Base_foo_defs )
|
|
864 |
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
|
|
865 |
simp add: mhead_resTy_simp)
|
|
866 |
done
|
|
867 |
|
|
868 |
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
|
|
869 |
apply (unfold Ext_foo_defs )
|
|
870 |
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
|
|
871 |
simp add: mhead_resTy_simp )
|
|
872 |
apply (rule wt.Cast)
|
|
873 |
prefer 2
|
|
874 |
apply simp
|
|
875 |
apply (rule_tac [2] narrow.subcls [THEN cast.narrow])
|
|
876 |
apply (auto intro!: wtIs)
|
|
877 |
done
|
|
878 |
|
|
879 |
declare mhead_resTy_simp [simp add]
|
|
880 |
declare member_is_static_simp [simp add]
|
|
881 |
|
|
882 |
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
|
|
883 |
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
|
|
884 |
apply (auto intro!: wf_Base_foo)
|
|
885 |
apply (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
|
|
886 |
apply (auto intro!: wtIs)
|
|
887 |
apply (auto simp add: Base_foo_defs entails_def Let_def)
|
|
888 |
apply (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
|
|
889 |
apply (insert Base_foo_no_hide , simp add: Base_foo_def,blast)
|
|
890 |
done
|
|
891 |
|
|
892 |
|
|
893 |
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
|
|
894 |
apply (unfold wf_cdecl_def ExtCl_def)
|
|
895 |
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
|
|
896 |
apply (auto simp add: entails_def snd_special_simp)
|
|
897 |
apply (insert Ext_foo_stat_override)
|
|
898 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
|
|
899 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
|
|
900 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
|
|
901 |
apply (insert Ext_foo_no_hide)
|
|
902 |
apply (simp_all add: qmdecl_def)
|
|
903 |
apply blast+
|
|
904 |
done
|
|
905 |
|
|
906 |
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
|
|
907 |
apply (simp (no_asm) add: Ifaces_def)
|
|
908 |
apply (simp (no_asm_simp))
|
|
909 |
apply (rule wf_HasFoo)
|
|
910 |
done
|
|
911 |
|
|
912 |
lemma wf_cdecl_all_standard_classes:
|
|
913 |
"Ball (set standard_classes) (wf_cdecl tprg)"
|
|
914 |
apply (unfold standard_classes_def Let_def
|
|
915 |
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
|
|
916 |
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
|
|
917 |
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
|
|
918 |
apply (auto simp add: Object_def Classes_def standard_classes_def
|
|
919 |
SXcptC_def SXcpt_def)
|
|
920 |
done
|
|
921 |
|
|
922 |
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
|
|
923 |
apply (simp (no_asm) add: Classes_def)
|
|
924 |
apply (simp (no_asm_simp))
|
|
925 |
apply (rule wf_BaseC [THEN conjI])
|
|
926 |
apply (rule wf_ExtC [THEN conjI])
|
|
927 |
apply (rule wf_cdecl_all_standard_classes)
|
|
928 |
done
|
|
929 |
|
|
930 |
theorem wf_tprg: "wf_prog tprg"
|
|
931 |
apply (unfold wf_prog_def Let_def)
|
|
932 |
apply (simp (no_asm) add: unique_ifaces unique_classes)
|
|
933 |
apply (rule conjI)
|
|
934 |
apply ((simp (no_asm) add: Classes_def standard_classes_def))
|
|
935 |
apply (rule conjI)
|
|
936 |
apply (simp add: Object_mdecls_def)
|
|
937 |
apply safe
|
|
938 |
apply (cut_tac xn_cases_old) (* FIXME (insert xn_cases) *)
|
|
939 |
apply (simp (no_asm_simp) add: Classes_def standard_classes_def)
|
|
940 |
apply (insert wf_idecl_all)
|
|
941 |
apply (insert wf_cdecl_all)
|
|
942 |
apply auto
|
|
943 |
done
|
|
944 |
|
|
945 |
|
|
946 |
section "max spec"
|
|
947 |
|
|
948 |
lemma appl_methds_Base_foo:
|
|
949 |
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =
|
|
950 |
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
|
|
951 |
,[Class Base])}"
|
|
952 |
apply (unfold appl_methds_def)
|
|
953 |
apply (simp (no_asm))
|
|
954 |
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
|
|
955 |
apply (auto simp add: cmheads_def Base_foo_defs)
|
|
956 |
done
|
|
957 |
|
|
958 |
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> =
|
|
959 |
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
|
|
960 |
, [Class Base])}"
|
|
961 |
apply (unfold max_spec_def)
|
|
962 |
apply (simp (no_asm) add: appl_methds_Base_foo)
|
|
963 |
apply auto
|
|
964 |
done
|
|
965 |
|
|
966 |
|
|
967 |
section "well-typedness"
|
|
968 |
|
|
969 |
lemma wt_test: "\<lparr>prg=tprg,cls=S,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
|
|
970 |
apply (unfold test_def arr_viewed_from_def)
|
|
971 |
(* ?pTs = [Class Base] *)
|
|
972 |
apply (rule wtIs (* ;; *))
|
|
973 |
apply (rule wtIs (* Ass *))
|
|
974 |
apply (rule wtIs (* NewC *))
|
|
975 |
apply (rule wtIs (* LVar *))
|
|
976 |
apply (simp)
|
|
977 |
apply (simp)
|
|
978 |
apply (simp)
|
|
979 |
apply (rule wtIs (* NewC *))
|
|
980 |
apply (simp)
|
|
981 |
apply (simp)
|
|
982 |
apply (rule wtIs (* Try *))
|
|
983 |
prefer 4
|
|
984 |
apply (simp)
|
|
985 |
defer
|
|
986 |
apply (rule wtIs (* Expr *))
|
|
987 |
apply (rule wtIs (* Call *))
|
|
988 |
apply (rule wtIs (* Acc *))
|
|
989 |
apply (rule wtIs (* LVar *))
|
|
990 |
apply (simp)
|
|
991 |
apply (simp)
|
|
992 |
apply (rule wtIs (* Cons *))
|
|
993 |
apply (rule wtIs (* Lit *))
|
|
994 |
apply (simp)
|
|
995 |
apply (rule wtIs (* Nil *))
|
|
996 |
apply (simp)
|
|
997 |
apply (rule max_spec_Base_foo)
|
|
998 |
apply (simp)
|
|
999 |
apply (simp)
|
|
1000 |
apply (simp)
|
|
1001 |
apply (simp)
|
|
1002 |
apply (rule wtIs (* While *))
|
|
1003 |
apply (rule wtIs (* Acc *))
|
|
1004 |
apply (rule wtIs (* AVar *))
|
|
1005 |
apply (rule wtIs (* Acc *))
|
|
1006 |
apply (rule wtIs (* FVar *))
|
|
1007 |
apply (rule wtIs (* StatRef *))
|
|
1008 |
apply (simp)
|
|
1009 |
apply (simp)
|
|
1010 |
apply (simp )
|
|
1011 |
apply (simp)
|
|
1012 |
apply (rule wtIs (* LVar *))
|
|
1013 |
apply (simp)
|
|
1014 |
apply (rule wtIs (* Skip *))
|
|
1015 |
done
|
|
1016 |
|
|
1017 |
|
|
1018 |
section "execution"
|
|
1019 |
|
|
1020 |
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>
|
|
1021 |
new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
|
|
1022 |
apply (frule atleast_free_SucD)
|
|
1023 |
apply (drule atleast_free_Suc [THEN iffD1])
|
|
1024 |
apply clarsimp
|
|
1025 |
apply (frule new_Addr_SomeI)
|
|
1026 |
apply force
|
|
1027 |
done
|
|
1028 |
|
|
1029 |
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
|
|
1030 |
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
|
|
1031 |
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
|
|
1032 |
Base_foo_defs [simp]
|
|
1033 |
|
|
1034 |
ML {* bind_thms ("eval_intros", map
|
|
1035 |
(simplify (simpset() delsimps [thm "Skip_eq"]
|
|
1036 |
addsimps [thm "lvar_def"]) o
|
|
1037 |
rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
|
|
1038 |
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
|
|
1039 |
|
|
1040 |
consts
|
|
1041 |
a :: loc
|
|
1042 |
b :: loc
|
|
1043 |
c :: loc
|
|
1044 |
|
|
1045 |
syntax
|
|
1046 |
|
|
1047 |
tprg :: prog
|
|
1048 |
|
|
1049 |
obj_a :: obj
|
|
1050 |
obj_b :: obj
|
|
1051 |
obj_c :: obj
|
|
1052 |
arr_N :: "(vn, val) table"
|
|
1053 |
arr_a :: "(vn, val) table"
|
|
1054 |
globs1 :: globs
|
|
1055 |
globs2 :: globs
|
|
1056 |
globs3 :: globs
|
|
1057 |
globs8 :: globs
|
|
1058 |
locs3 :: locals
|
|
1059 |
locs4 :: locals
|
|
1060 |
locs8 :: locals
|
|
1061 |
s0 :: state
|
|
1062 |
s0' :: state
|
|
1063 |
s9' :: state
|
|
1064 |
s1 :: state
|
|
1065 |
s1' :: state
|
|
1066 |
s2 :: state
|
|
1067 |
s2' :: state
|
|
1068 |
s3 :: state
|
|
1069 |
s3' :: state
|
|
1070 |
s4 :: state
|
|
1071 |
s4' :: state
|
|
1072 |
s6' :: state
|
|
1073 |
s7' :: state
|
|
1074 |
s8 :: state
|
|
1075 |
s8' :: state
|
|
1076 |
|
|
1077 |
translations
|
|
1078 |
|
|
1079 |
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
|
|
1080 |
|
|
1081 |
"obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) two
|
|
1082 |
,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
|
|
1083 |
"obj_b" <= "\<lparr>tag=CInst Ext
|
|
1084 |
,values=(empty(Inl (vee, Base)\<mapsto>Null )
|
|
1085 |
(Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
|
|
1086 |
"obj_c" == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
|
|
1087 |
"arr_N" == "empty(Inl (arr, Base)\<mapsto>Null)"
|
|
1088 |
"arr_a" == "empty(Inl (arr, Base)\<mapsto>Addr a)"
|
|
1089 |
"globs1" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
|
|
1090 |
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
|
|
1091 |
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
|
|
1092 |
"globs2" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
|
|
1093 |
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
|
|
1094 |
(Inl a\<mapsto>obj_a)
|
|
1095 |
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
|
|
1096 |
"globs3" == "globs2(Inl b\<mapsto>obj_b)"
|
|
1097 |
"globs8" == "globs3(Inl c\<mapsto>obj_c)"
|
|
1098 |
"locs3" == "empty(VName e\<mapsto>Addr b)"
|
|
1099 |
"locs4" == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
|
|
1100 |
"locs8" == "locs3(VName z\<mapsto>Addr c)"
|
|
1101 |
"s0" == " st empty empty"
|
|
1102 |
"s0'" == " Norm s0"
|
|
1103 |
"s1" == " st globs1 empty"
|
|
1104 |
"s1'" == " Norm s1"
|
|
1105 |
"s2" == " st globs2 empty"
|
|
1106 |
"s2'" == " Norm s2"
|
|
1107 |
"s3" == " st globs3 locs3 "
|
|
1108 |
"s3'" == " Norm s3"
|
|
1109 |
"s4" == " st globs3 locs4"
|
|
1110 |
"s4'" == " Norm s4"
|
|
1111 |
"s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
|
|
1112 |
"s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
|
|
1113 |
"s8" == " st globs8 locs8"
|
|
1114 |
"s8'" == " Norm s8"
|
|
1115 |
"s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
|
|
1116 |
|
|
1117 |
|
|
1118 |
syntax "four"::nat
|
|
1119 |
"tree"::nat
|
|
1120 |
"two" ::nat
|
|
1121 |
"one" ::nat
|
|
1122 |
translations
|
|
1123 |
"one" == "Suc 0"
|
|
1124 |
"two" == "Suc one"
|
|
1125 |
"tree" == "Suc two"
|
|
1126 |
"four" == "Suc tree"
|
|
1127 |
|
|
1128 |
declare Pair_eq [simp del]
|
|
1129 |
lemma exec_test:
|
|
1130 |
"\<lbrakk>the (new_Addr (heap s1)) = a;
|
|
1131 |
the (new_Addr (heap ?s2)) = b;
|
|
1132 |
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>
|
|
1133 |
atleast_free (heap s0) four \<Longrightarrow>
|
|
1134 |
tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
|
|
1135 |
apply (unfold test_def arr_viewed_from_def)
|
|
1136 |
(* ?s9' = s9' *)
|
|
1137 |
apply (simp (no_asm_use))
|
|
1138 |
apply (drule (1) alloc_one,clarsimp)
|
|
1139 |
apply (rule eval_Is (* ;; *))
|
|
1140 |
apply (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
|
|
1141 |
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
|
|
1142 |
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
|
|
1143 |
apply (rule eval_Is (* Expr *))
|
|
1144 |
apply (rule eval_Is (* Ass *))
|
|
1145 |
apply (rule eval_Is (* LVar *))
|
|
1146 |
apply (rule eval_Is (* NewC *))
|
|
1147 |
(* begin init Ext *)
|
|
1148 |
apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
|
|
1149 |
apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
|
|
1150 |
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
|
|
1151 |
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
|
|
1152 |
apply (rule eval_Is (* Init Ext *))
|
|
1153 |
apply (simp)
|
|
1154 |
apply (rule conjI)
|
|
1155 |
prefer 2 apply (rule conjI HOL.refl)+
|
|
1156 |
apply (rule eval_Is (* Init Base *))
|
|
1157 |
apply (simp add: arr_viewed_from_def)
|
|
1158 |
apply (rule conjI)
|
|
1159 |
apply (rule eval_Is (* Init Object *))
|
|
1160 |
apply (simp)
|
|
1161 |
apply (rule conjI, rule HOL.refl)+
|
|
1162 |
apply (rule HOL.refl)
|
|
1163 |
apply (simp)
|
|
1164 |
apply (rule conjI, rule_tac [2] HOL.refl)
|
|
1165 |
apply (rule eval_Is (* Expr *))
|
|
1166 |
apply (rule eval_Is (* Ass *))
|
|
1167 |
apply (rule eval_Is (* FVar *))
|
|
1168 |
apply (rule init_done, simp)
|
|
1169 |
apply (rule eval_Is (* StatRef *))
|
|
1170 |
apply (simp)
|
|
1171 |
apply (rule eval_Is (* NewA *))
|
|
1172 |
apply (simp)
|
|
1173 |
apply (rule eval_Is (* Lit *))
|
|
1174 |
apply (simp)
|
|
1175 |
apply (rule halloc.New)
|
|
1176 |
apply (simp (no_asm_simp))
|
|
1177 |
apply (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
|
|
1178 |
apply (simp (no_asm_simp))
|
|
1179 |
apply (simp add: upd_gobj_def)
|
|
1180 |
(* end init Ext *)
|
|
1181 |
apply (rule halloc.New)
|
|
1182 |
apply (drule alloc_one)
|
|
1183 |
prefer 2 apply fast
|
|
1184 |
apply (simp (no_asm_simp))
|
|
1185 |
apply (drule atleast_free_weaken)
|
|
1186 |
apply force
|
|
1187 |
apply (simp)
|
|
1188 |
apply (drule alloc_one)
|
|
1189 |
apply (simp (no_asm_simp))
|
|
1190 |
apply clarsimp
|
|
1191 |
apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
|
|
1192 |
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
|
|
1193 |
apply (simp (no_asm_use))
|
|
1194 |
apply (rule eval_Is (* Try *))
|
|
1195 |
apply (rule eval_Is (* Expr *))
|
|
1196 |
(* begin method call *)
|
|
1197 |
apply (rule eval_Is (* Call *))
|
|
1198 |
apply (rule eval_Is (* Acc *))
|
|
1199 |
apply (rule eval_Is (* LVar *))
|
|
1200 |
apply (rule eval_Is (* Cons *))
|
|
1201 |
apply (rule eval_Is (* Lit *))
|
|
1202 |
apply (rule eval_Is (* Nil *))
|
|
1203 |
apply (simp)
|
|
1204 |
apply (simp)
|
|
1205 |
apply (rule eval_Is (* Methd *))
|
|
1206 |
apply (simp add: body_def Let_def)
|
|
1207 |
apply (rule eval_Is (* Body *))
|
|
1208 |
apply (rule init_done, simp)
|
|
1209 |
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
|
|
1210 |
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
|
|
1211 |
apply (rule eval_Is (* Expr *))
|
|
1212 |
apply (rule eval_Is (* Ass *))
|
|
1213 |
apply (rule eval_Is (* FVar *))
|
|
1214 |
apply (rule init_done, simp)
|
|
1215 |
apply (rule eval_Is (* Cast *))
|
|
1216 |
apply (rule eval_Is (* Acc *))
|
|
1217 |
apply (rule eval_Is (* LVar *))
|
|
1218 |
apply (simp)
|
|
1219 |
apply (simp split del: split_if)
|
|
1220 |
apply (rule eval_Is (* XcptE *))
|
|
1221 |
apply (simp)
|
|
1222 |
(* end method call *)
|
|
1223 |
apply (rule sxalloc.intros)
|
|
1224 |
apply (rule halloc.New)
|
|
1225 |
apply (erule alloc_one [THEN conjunct1])
|
|
1226 |
apply (simp (no_asm_simp))
|
|
1227 |
apply (simp (no_asm_simp))
|
|
1228 |
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
|
|
1229 |
apply (drule alloc_one [THEN conjunct1])
|
|
1230 |
apply (simp (no_asm_simp))
|
|
1231 |
apply (erule_tac V = "atleast_free ?h two" in thin_rl)
|
|
1232 |
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
|
|
1233 |
apply simp
|
|
1234 |
apply (rule eval_Is (* While *))
|
|
1235 |
apply (rule eval_Is (* Acc *))
|
|
1236 |
apply (rule eval_Is (* AVar *))
|
|
1237 |
apply (rule eval_Is (* Acc *))
|
|
1238 |
apply (rule eval_Is (* FVar *))
|
|
1239 |
apply (rule init_done, simp)
|
|
1240 |
apply (rule eval_Is (* StatRef *))
|
|
1241 |
apply (simp)
|
|
1242 |
apply (rule eval_Is (* Lit *))
|
|
1243 |
apply (simp (no_asm_simp))
|
|
1244 |
apply (auto simp add: in_bounds_def)
|
|
1245 |
done
|
|
1246 |
declare Pair_eq [simp]
|
|
1247 |
|
|
1248 |
end
|