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