26 e.foo(null); |
26 e.foo(null); |
27 } |
27 } |
28 } |
28 } |
29 *) |
29 *) |
30 |
30 |
31 Example = Eval + |
31 theory Example = Eval: |
32 |
32 |
33 datatype cnam_ = Base_ | Ext_ |
33 datatype cnam_ = Base_ | Ext_ |
34 datatype vnam_ = vee_ | x_ | e_ |
34 datatype vnam_ = vee_ | x_ | e_ |
35 |
35 |
36 consts |
36 consts |
37 |
37 |
38 cnam_ :: "cnam_ => cname" |
38 cnam_ :: "cnam_ => cname" |
39 vnam_ :: "vnam_ => vnam" |
39 vnam_ :: "vnam_ => vnam" |
40 |
40 |
41 rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *) |
41 axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *) |
42 |
42 |
43 inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)" |
43 inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)" |
44 inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)" |
44 inj_vnam_: "(vnam_ x = vnam_ y) = (x = y)" |
45 |
45 |
46 surj_cnam_ "\\<exists>m. n = cnam_ m" |
46 surj_cnam_: "\<exists>m. n = cnam_ m" |
47 surj_vnam_ "\\<exists>m. n = vnam_ m" |
47 surj_vnam_: "\<exists>m. n = vnam_ m" |
|
48 |
|
49 declare inj_cnam_ [simp] inj_vnam_ [simp] |
48 |
50 |
49 syntax |
51 syntax |
50 |
52 |
51 Base, Ext :: cname |
53 Base :: cname |
52 vee, x, e :: vname |
54 Ext :: cname |
|
55 vee :: vname |
|
56 x :: vname |
|
57 e :: vname |
53 |
58 |
54 translations |
59 translations |
55 |
60 |
56 "Base" == "cnam_ Base_" |
61 "Base" == "cnam_ Base_" |
57 "Ext" == "cnam_ Ext_" |
62 "Ext" == "cnam_ Ext_" |
58 "vee" == "VName (vnam_ vee_)" |
63 "vee" == "VName (vnam_ vee_)" |
59 "x" == "VName (vnam_ x_)" |
64 "x" == "VName (vnam_ x_)" |
60 "e" == "VName (vnam_ e_)" |
65 "e" == "VName (vnam_ e_)" |
61 |
66 |
62 rules |
67 axioms |
63 Base_not_Object "Base \\<noteq> Object" |
68 |
64 Ext_not_Object "Ext \\<noteq> Object" |
69 Base_not_Object: "Base \<noteq> Object" |
|
70 Ext_not_Object: "Ext \<noteq> Object" |
|
71 |
|
72 declare Base_not_Object [simp] Ext_not_Object [simp] |
|
73 declare Base_not_Object [THEN not_sym, simp] |
|
74 declare Ext_not_Object [THEN not_sym, simp] |
65 |
75 |
66 consts |
76 consts |
67 |
77 |
68 foo_Base :: java_mb |
78 foo_Base:: java_mb |
69 foo_Ext :: java_mb |
79 foo_Ext :: java_mb |
70 BaseC, ExtC :: java_mb cdecl |
80 BaseC :: "java_mb cdecl" |
71 test :: stmt |
81 ExtC :: "java_mb cdecl" |
72 foo :: mname |
82 test :: stmt |
73 a,b :: loc |
83 foo :: mname |
|
84 a :: loc |
|
85 b :: loc |
74 |
86 |
75 defs |
87 defs |
76 |
88 |
77 foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)" |
89 foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)" |
78 BaseC_def "BaseC == (Base, (Object, |
90 BaseC_def:"BaseC == (Base, (Object, |
79 [(vee, PrimT Boolean)], |
91 [(vee, PrimT Boolean)], |
80 [((foo,[Class Base]),Class Base,foo_Base)]))" |
92 [((foo,[Class Base]),Class Base,foo_Base)]))" |
81 foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext |
93 foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext |
82 (LAcc x)..vee:=Lit (Intg #1)), |
94 (LAcc x)..vee:=Lit (Intg #1)), |
83 Lit Null)" |
95 Lit Null)" |
84 ExtC_def "ExtC == (Ext, (Base , |
96 ExtC_def: "ExtC == (Ext, (Base , |
85 [(vee, PrimT Integer)], |
97 [(vee, PrimT Integer)], |
86 [((foo,[Class Base]),Class Ext,foo_Ext)]))" |
98 [((foo,[Class Base]),Class Ext,foo_Ext)]))" |
87 |
99 |
88 test_def "test == Expr(e::=NewC Ext);; |
100 test_def:"test == Expr(e::=NewC Ext);; |
89 Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
101 Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
90 |
102 |
91 |
103 |
92 syntax |
104 syntax |
93 |
105 |
94 NP :: xcpt |
106 NP :: xcpt |
95 tprg :: java_mb prog |
107 tprg ::"java_mb prog" |
96 obj1, obj2 :: obj |
108 obj1 :: obj |
97 s0,s1,s2,s3,s4:: state |
109 obj2 :: obj |
|
110 s0 :: state |
|
111 s1 :: state |
|
112 s2 :: state |
|
113 s3 :: state |
|
114 s4 :: state |
98 |
115 |
99 translations |
116 translations |
100 |
117 |
101 "NP" == "NullPointer" |
118 "NP" == "NullPointer" |
102 "tprg" == "[ObjectC, BaseC, ExtC]" |
119 "tprg" == "[ObjectC, BaseC, ExtC]" |
103 "obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False) |
120 "obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False) |
104 ((vee, Ext )\\<mapsto>Intg #0))" |
121 ((vee, Ext )\<mapsto>Intg #0))" |
105 "s0" == " Norm (empty, empty)" |
122 "s0" == " Norm (empty, empty)" |
106 "s1" == " Norm (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))" |
123 "s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
107 "s2" == " Norm (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))" |
124 "s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
108 "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))" |
125 "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
|
126 |
|
127 |
|
128 ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *} |
|
129 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
|
130 apply (simp (no_asm)) |
|
131 done |
|
132 lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa" |
|
133 apply (simp (no_asm_simp)) |
|
134 done |
|
135 declare map_of_Cons [simp del]; (* sic! *) |
|
136 |
|
137 lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])" |
|
138 apply (unfold ObjectC_def class_def) |
|
139 apply (simp (no_asm)) |
|
140 done |
|
141 |
|
142 lemma class_tprg_Base [simp]: |
|
143 "class tprg Base = Some (Object, |
|
144 [(vee, PrimT Boolean)], |
|
145 [((foo, [Class Base]), Class Base, foo_Base)])" |
|
146 apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
|
147 apply (simp (no_asm)) |
|
148 done |
|
149 |
|
150 lemma class_tprg_Ext [simp]: |
|
151 "class tprg Ext = Some (Base, |
|
152 [(vee, PrimT Integer)], |
|
153 [((foo, [Class Base]), Class Ext, foo_Ext)])" |
|
154 apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
|
155 apply (simp (no_asm)) |
|
156 done |
|
157 |
|
158 lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R" |
|
159 apply (auto dest!: tranclD subcls1D) |
|
160 done |
|
161 |
|
162 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" |
|
163 apply (erule rtrancl_induct) |
|
164 apply auto |
|
165 apply (drule subcls1D) |
|
166 apply auto |
|
167 done |
|
168 |
|
169 lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R" |
|
170 apply (auto dest!: tranclD subcls1D) |
|
171 done |
|
172 |
|
173 lemma class_tprgD: |
|
174 "class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext" |
|
175 apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
|
176 apply (auto split add: split_if_asm simp add: map_of_Cons) |
|
177 done |
|
178 |
|
179 lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R" |
|
180 apply (auto dest!: tranclD subcls1D) |
|
181 apply (frule class_tprgD) |
|
182 apply (auto dest!:) |
|
183 apply (drule rtranclD) |
|
184 apply auto |
|
185 done |
|
186 |
|
187 lemma unique_classes: "unique tprg" |
|
188 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def) |
|
189 done |
|
190 |
|
191 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl] |
|
192 |
|
193 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base" |
|
194 apply (rule subcls_direct) |
|
195 apply auto |
|
196 done |
|
197 |
|
198 lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base" |
|
199 apply (rule widen.subcls) |
|
200 apply (simp (no_asm)) |
|
201 done |
|
202 |
|
203 declare ty_expr_ty_exprs_wt_stmt.intros [intro!] |
|
204 |
|
205 lemma acyclic_subcls1_: "acyclic (subcls1 tprg)" |
|
206 apply (rule acyclicI) |
|
207 apply safe |
|
208 done |
|
209 |
|
210 lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]] |
|
211 |
|
212 lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma] |
|
213 |
|
214 lemma fields_Object [simp]: "fields (tprg, Object) = []" |
|
215 apply (subst fields_rec_) |
|
216 apply auto |
|
217 done |
|
218 |
|
219 declare is_class_def [simp] |
|
220 |
|
221 lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]" |
|
222 apply (subst fields_rec_) |
|
223 apply auto |
|
224 done |
|
225 |
|
226 lemma fields_Ext [simp]: |
|
227 "fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)" |
|
228 apply (rule trans) |
|
229 apply (rule fields_rec_) |
|
230 apply auto |
|
231 done |
|
232 |
|
233 lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma] |
|
234 |
|
235 lemma method_Object [simp]: "method (tprg,Object) = map_of []" |
|
236 apply (subst method_rec_) |
|
237 apply auto |
|
238 done |
|
239 |
|
240 lemma method_Base [simp]: "method (tprg, Base) = map_of |
|
241 [((foo, [Class Base]), Base, (Class Base, foo_Base))]" |
|
242 apply (rule trans) |
|
243 apply (rule method_rec_) |
|
244 apply auto |
|
245 done |
|
246 |
|
247 lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of |
|
248 [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])" |
|
249 apply (rule trans) |
|
250 apply (rule method_rec_) |
|
251 apply auto |
|
252 done |
|
253 |
|
254 lemma wf_foo_Base: |
|
255 "wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))" |
|
256 apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def) |
|
257 apply auto |
|
258 done |
|
259 |
|
260 lemma wf_foo_Ext: |
|
261 "wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))" |
|
262 apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def) |
|
263 apply auto |
|
264 apply (rule ty_expr_ty_exprs_wt_stmt.Cast) |
|
265 prefer 2 |
|
266 apply (simp) |
|
267 apply (rule_tac [2] cast.subcls) |
|
268 apply (unfold field_def) |
|
269 apply auto |
|
270 done |
|
271 |
|
272 lemma wf_ObjectC: |
|
273 "wf_cdecl wf_java_mdecl tprg ObjectC" |
|
274 apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def) |
|
275 apply (simp (no_asm)) |
|
276 done |
|
277 |
|
278 lemma wf_BaseC: |
|
279 "wf_cdecl wf_java_mdecl tprg BaseC" |
|
280 apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def) |
|
281 apply (simp (no_asm)) |
|
282 apply (fold BaseC_def) |
|
283 apply (rule wf_foo_Base [THEN conjI]) |
|
284 apply auto |
|
285 done |
|
286 |
|
287 lemma wf_ExtC: |
|
288 "wf_cdecl wf_java_mdecl tprg ExtC" |
|
289 apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def) |
|
290 apply (simp (no_asm)) |
|
291 apply (fold ExtC_def) |
|
292 apply (rule wf_foo_Ext [THEN conjI]) |
|
293 apply auto |
|
294 apply (drule rtranclD) |
|
295 apply auto |
|
296 done |
|
297 |
|
298 lemma wf_tprg: |
|
299 "wf_prog wf_java_mdecl tprg" |
|
300 apply (unfold wf_prog_def Let_def) |
|
301 apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes) |
|
302 done |
|
303 |
|
304 lemma appl_methds_foo_Base: |
|
305 "appl_methds tprg Base (foo, [NT]) = |
|
306 {((Class Base, Class Base), [Class Base])}" |
|
307 apply (unfold appl_methds_def) |
|
308 apply (simp (no_asm)) |
|
309 apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base") |
|
310 apply (auto simp add: map_of_Cons foo_Base_def) |
|
311 done |
|
312 |
|
313 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) = |
|
314 {((Class Base, Class Base), [Class Base])}" |
|
315 apply (unfold max_spec_def) |
|
316 apply (auto simp add: appl_methds_foo_Base) |
|
317 done |
|
318 |
|
319 ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *} |
|
320 lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
|
321 Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" |
|
322 apply (tactic t) (* ;; *) |
|
323 apply (tactic t) (* Expr *) |
|
324 apply (tactic t) (* LAss *) |
|
325 apply (tactic t) (* LAcc *) |
|
326 apply (simp (no_asm)) |
|
327 apply (simp (no_asm)) |
|
328 apply (tactic t) (* NewC *) |
|
329 apply (simp (no_asm)) |
|
330 apply (simp (no_asm)) |
|
331 apply (tactic t) (* Expr *) |
|
332 apply (tactic t) (* Call *) |
|
333 apply (tactic t) (* LAcc *) |
|
334 apply (simp (no_asm)) |
|
335 apply (simp (no_asm)) |
|
336 apply (tactic t) (* Cons *) |
|
337 apply (tactic t) (* Lit *) |
|
338 apply (simp (no_asm)) |
|
339 apply (tactic t) (* Nil *) |
|
340 apply (simp (no_asm)) |
|
341 apply (rule max_spec_foo_Base) |
|
342 done |
|
343 |
|
344 ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *} |
|
345 |
|
346 declare split_if [split del] |
|
347 declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp] |
|
348 lemma exec_test: |
|
349 " [|new_Addr (heap (snd s0)) = (a, None)|] ==> |
|
350 tprg\<turnstile>s0 -test-> ?s" |
|
351 apply (unfold test_def) |
|
352 (* ?s = s3 *) |
|
353 apply (tactic e) (* ;; *) |
|
354 apply (tactic e) (* Expr *) |
|
355 apply (tactic e) (* LAss *) |
|
356 apply (tactic e) (* NewC *) |
|
357 apply force |
|
358 apply force |
|
359 apply (simp (no_asm)) |
|
360 apply (erule thin_rl) |
|
361 apply (tactic e) (* Expr *) |
|
362 apply (tactic e) (* Call *) |
|
363 apply (tactic e) (* LAcc *) |
|
364 apply force |
|
365 apply (tactic e) (* Cons *) |
|
366 apply (tactic e) (* Lit *) |
|
367 apply (tactic e) (* Nil *) |
|
368 apply (simp (no_asm)) |
|
369 apply (force simp add: foo_Ext_def) |
|
370 apply (simp (no_asm)) |
|
371 apply (tactic e) (* Expr *) |
|
372 apply (tactic e) (* FAss *) |
|
373 apply (tactic e) (* Cast *) |
|
374 apply (tactic e) (* LAcc *) |
|
375 apply (simp (no_asm)) |
|
376 apply (simp (no_asm)) |
|
377 apply (simp (no_asm)) |
|
378 apply (tactic e) (* XcptE *) |
|
379 apply (simp (no_asm)) |
|
380 apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force) |
|
381 apply (simp (no_asm)) |
|
382 apply (simp (no_asm)) |
|
383 apply (tactic e) (* XcptE *) |
|
384 done |
|
385 |
109 end |
386 end |