Added conditional and (&&) and or (||).
1 (* Title: HOL/Bali/Eval.thy
3 Author: David von Oheimb
4 License: GPL (GNU GENERAL PUBLIC LICENSE)
6 header {* Operational evaluation (big-step) semantics of Java expressions and
10 theory Eval = State + DeclConcepts:
14 improvements over Java Specification 1.0:
16 \item dynamic method lookup does not need to consider the return type
18 \item throw raises a NullPointer exception if a null reference is given, and
19 each throw of a standard exception yield a fresh exception object
21 \item if there is not enough memory even to allocate an OutOfMemory exception,
22 evaluation/execution fails, i.e. simply stops (was not specified)
23 \item array assignment checks lhs (and may throw exceptions) before evaluating
25 \item fixed exact positions of class initializations
26 (immediate at first active use)
31 \item evaluation vs. (single-step) transition semantics
32 evaluation semantics chosen, because:
34 \item[++] less verbose and therefore easier to read (and to handle in proofs)
35 \item[+] more abstract
36 \item[+] intermediate values (appearing in recursive rules) need not be
37 stored explicitly, e.g. no call body construct or stack of invocation
38 frames containing local variables and return addresses for method calls
40 \item[+] convenient rule induction for subject reduction theorem
41 \item[-] no interleaving (for parallelism) can be described
42 \item[-] stating a property of infinite executions requires the meta-level
43 argument that this property holds for any finite prefixes of it
44 (e.g. stopped using a counter that is decremented to zero and then
45 throwing an exception)
47 \item unified evaluation for variables, expressions, expression lists,
49 \item the value entry in statement rules is redundant
50 \item the value entry in rules is irrelevant in case of exceptions, but its full
51 inclusion helps to make the rule structure independent of exception occurence.
52 \item as irrelevant value entries are ignored, it does not matter if they are
54 For simplicity, (fixed) arbitrary values are preferred over "free" values.
55 \item the rule format is such that the start state may contain an exception.
57 \item[++] faciliates exception handling
60 \item the rules are defined carefully in order to be applicable even in not
61 type-correct situations (yielding undefined values),
62 e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
65 \item[-] less readable because of auxiliary functions like @{text the_Addr}
67 Alternative: "defensive" evaluation throwing some InternalError exception
68 in case of (impossible, for correct programs) type mismatches
69 \item there is exactly one rule per syntactic construct
71 \item[+] no redundancy in case distinctions
73 \item halloc fails iff there is no free heap address. When there is
74 only one free heap address left, it returns an OutOfMemory exception.
75 In this way it is guaranteed that when an OutOfMemory exception is thrown for
76 the first time, there is a free location on the heap to allocate it.
77 \item the allocation of objects that represent standard exceptions is deferred
78 until execution of any enclosing catch clause, which is transparent to
81 \item[-] requires an auxiliary execution relation
82 \item[++] avoids copies of allocation code and awkward case distinctions
83 (whether there is enough memory to allocate the exception) in
86 \item unfortunately @{text new_Addr} is not directly executable because of
91 \item local variables are initialized with default values
92 (no definite assignment)
93 \item garbage collection not considered, therefore also no finalizers
94 \item stack overflow and memory overflow during class initialization not
96 \item exceptions in initializations not replaced by ExceptionInInitializerError
100 types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
101 vals = "(val, vvar, val list) sum3"
103 "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
104 "vals" <= (type)"(val, vvar, val list) sum3"
107 dummy_res :: "vals" ("\<diamondsuit>")
109 "\<diamondsuit>" == "In1 Unit"
112 arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
113 "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
114 (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
116 lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
117 by (simp add: arbitrary3_def)
119 lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
120 by (simp add: arbitrary3_def)
122 lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary"
123 by (simp add: arbitrary3_def)
125 lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary"
126 by (simp add: arbitrary3_def)
129 section "exception throwing and catching"
132 throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
133 "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
136 "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
137 apply (unfold throw_def)
138 apply (simp (no_asm))
142 fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
143 "G,s\<turnstile>a' fits T \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
145 lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
146 by (simp add: fits_def)
149 lemma fits_Addr_RefT [simp]:
150 "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
151 by (simp add: fits_def)
153 lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>
154 (\<exists>t. T = RefT t) \<and> a' = Null \<or>
155 (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and> G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
156 apply (unfold fits_def)
157 apply (case_tac "\<exists>pt. T = PrimT pt")
161 apply (case_tac "a' = Null")
166 catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60)
167 "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and>
168 G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
170 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
171 apply (unfold catch_def)
172 apply (simp (no_asm))
175 lemma catch_XcptLoc [simp]:
176 "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
177 apply (unfold catch_def)
178 apply (simp (no_asm))
182 new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state"
183 "new_xcpt_var vn \<equiv>
184 \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
186 lemma new_xcpt_var_def2 [simp]:
187 "new_xcpt_var vn (x,s) =
188 Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
189 apply (unfold new_xcpt_var_def)
190 apply (simp (no_asm))
199 assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state"
200 "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
201 in (x',if x' = None then s' else s)"
204 lemma assign_Norm_Norm [simp]:
205 "f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>
206 \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
207 by (simp add: assign_def Let_def)
210 lemma assign_Norm_Norm [simp]:
211 "f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
212 by (simp add: assign_def Let_def)
215 lemma assign_Norm_Some [simp]:
216 "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk>
217 \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
218 by (simp add: assign_def Let_def split_beta)
221 lemma assign_Norm_Some [simp]:
222 "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk>
223 \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
224 by (simp add: assign_def Let_def split_beta)
227 lemma assign_Some [simp]:
228 "assign f v (Some x,s) = (Some x,s)"
229 by (simp add: assign_def Let_def split_beta)
231 lemma assign_supd [simp]:
232 "assign (\<lambda>v. supd (f v)) v (x,s)
233 = (x, if x = None then f v s else s)"
237 lemma assign_raise_if [simp]:
238 "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =
239 (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
240 apply (case_tac "x = None")
245 lemma assign_raise_if [simp]:
246 "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
247 store = f v (store s)\<rparr>) v s =
248 \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
249 store= if (abrupt s)=None \<and> \<not>b (store s) v
250 then f v (store s) else (store s)\<rparr>"
251 apply (case_tac "abrupt s = None")
258 init_comp_ty :: "ty \<Rightarrow> stmt"
259 "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
261 lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
262 apply (unfold init_comp_ty_def)
263 apply (simp (no_asm))
269 target :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
271 \<equiv> if m = IntVir
272 then obj_class (lookup_obj s a')
273 else the_Class (RefT t)"
276 invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
277 "invocation_class m s a' statT
279 Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC)
280 then the_Class (RefT statT)
282 | SuperM \<Rightarrow> the_Class (RefT statT)
283 | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
285 invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname"
286 "invocation_declclass G m s a' statT sig
287 \<equiv> declclass (the (dynlookup G statT
288 (invocation_class m s a' statT)
291 lemma invocation_class_IntVir [simp]:
292 "invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
293 by (simp add: invocation_class_def)
295 lemma dynclass_SuperM [simp]:
296 "invocation_class SuperM s a' statT = the_Class (RefT statT)"
297 by (simp add: invocation_class_def)
299 lemma invocation_class_notIntVir [simp]:
300 "m \<noteq> IntVir \<Longrightarrow> invocation_class m s a' statT = the_Class (RefT statT)"
301 by (simp add: invocation_class_def)
304 lemma invocation_class_Static [simp]:
305 "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC)
306 then the_Class (RefT statT)
308 by (simp add: invocation_class_def)
311 init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
312 state \<Rightarrow> state"
313 "init_lvars G C sig mode a' pvs
314 \<equiv> \<lambda> (x,s).
315 let m = mthd (the (methd G C sig));
319 \<Rightarrow> (case e of
320 VNam v \<Rightarrow> (init_vals (table_of (lcls (mbody m)))
321 ((pars m)[\<mapsto>]pvs)) v
322 | Res \<Rightarrow> Some (default_val (resTy m)))
324 \<Rightarrow> (if mode=Static then None else Some a'))
325 in set_lvars l (if mode = Static then x else np a' x,s)"
329 lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =
334 \<Rightarrow> (case e of
336 \<Rightarrow> (init_vals
337 (table_of (lcls (mbody (mthd (the (methd G C sig))))))
338 ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
339 | Res \<Rightarrow> Some (default_val (resTy (mthd (the (methd G C sig))))))
341 \<Rightarrow> (if mode=Static then None else Some a')))
342 (if mode = Static then x else np a' x,s)"
343 apply (unfold init_lvars_def)
344 apply (simp (no_asm) add: Let_def)
348 body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr"
349 "body G C sig \<equiv> let m = the (methd G C sig)
350 in Body (declclass m) (stmt (mbody (mthd m)))"
353 "body G C sig = Body (declclass (the (methd G C sig)))
354 (stmt (mbody (mthd (the (methd G C sig)))))"
355 apply (unfold body_def Let_def)
363 lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
364 "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
366 fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
368 \<equiv> let (oref,xf) = if stat then (Stat C,id)
369 else (Heap (the_Addr a'),np a');
371 f = (\<lambda>v. supd (upd_gobj oref n v))
372 in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
375 \<equiv> let (oref,xf) = if stat then (Stat C,id)
376 else (Heap (the_Addr a'),np a');
378 f = (\<lambda>v. supd (upd_gobj oref n v))
379 in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
381 avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
383 \<equiv> let oref = Heap (the_Addr a');
386 (T,k,cs) = the_Arr (globs (store s) oref);
387 f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T)
389 ,upd_gobj oref n v s))
391 ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
393 lemma fvar_def2: "fvar C stat fn a' s =
396 (the (globs (store s) (if stat then Stat C else Heap (the_Addr a'))))
398 ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a'))
401 ,abupd (if stat then id else np a') s)
403 apply (unfold fvar_def)
404 apply (simp (no_asm) add: Let_def split_beta)
407 lemma avar_def2: "avar G i' a' s =
408 ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a'))))))
410 ,(\<lambda>v (x,s'). (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
411 (Heap (the_Addr a'))))))
413 ,upd_gobj (Heap (the_Addr a'))
414 (Inr (the_Intg i')) v s')))
415 ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s)
416 (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
418 apply (unfold avar_def)
419 apply (simp (no_asm) add: Let_def split_beta)
424 "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
425 "check_field_access G accC statDeclC fn stat a' s
426 \<equiv> let oref = if stat then Stat statDeclC
427 else Heap (the_Addr a');
429 Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
430 | Stat C \<Rightarrow> C;
431 f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
433 (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
438 check_method_access::
439 "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
440 "check_method_access G accC statT mode sig a' s
441 \<equiv> let invC = invocation_class mode (store s) a' statT;
442 dynM = the (dynlookup G statT invC sig)
444 (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
448 section "evaluation judgments"
450 consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
452 "eval_unop UPlus v = Intg (the_Intg v)"
453 "eval_unop UMinus v = Intg (- (the_Intg v))"
454 "eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
455 "eval_unop UNot v = Bool (\<not> the_Bool v)"
457 consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
459 "eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
460 "eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
461 "eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
462 "eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
463 "eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
465 -- "Be aware of the explicit coercion of the shift distance to nat"
466 "eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
467 "eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
468 "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
470 "eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
471 "eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
472 "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
473 "eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
475 "eval_binop Eq v1 v2 = Bool (v1=v2)"
476 "eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)"
477 "eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
478 "eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
479 "eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
480 "eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
481 "eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
482 "eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
483 "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
484 "eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
486 constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
487 "need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<or>
488 (binop=CondOr \<and> the_Bool v1))"
489 text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
490 if the value isn't already determined by the first argument*}
492 lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b"
493 by (simp add: need_second_arg_def)
495 lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)"
496 by (simp add: need_second_arg_def)
498 lemma need_second_arg_strict[simp]:
499 "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
501 (simp_all add: need_second_arg_def)
504 eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set"
505 halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set"
506 sxalloc:: "prog \<Rightarrow> (state \<times> state) set"
510 eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _" [61,61,80, 61]60)
511 exec ::"[prog,state,stmt ,state]=>bool"("_|-_ -_-> _" [61,61,65, 61]60)
512 evar ::"[prog,state,var ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
513 eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
514 evals::"[prog,state,expr list ,
515 val list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
516 hallo::"[prog,state,obj_tag,
517 loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
518 sallo::"[prog,state ,state]=>bool"("_|-_ -sxalloc-> _"[61,61, 61]60)
521 eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _" [61,61,80, 61]60)
522 exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60)
523 evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
524 eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
525 evals::"[prog,state,expr list ,
526 val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
527 hallo::"[prog,state,obj_tag,
528 loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
529 sallo::"[prog,state, state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61, 61]60)
532 "G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> w___s' " == "(s,t,w___s') \<in> eval G"
533 "G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w, s')" <= "(s,t,w, s') \<in> eval G"
534 "G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
535 "G\<turnstile>s \<midarrow>c \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
536 "G\<turnstile>s \<midarrow>c \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit> , s')"
537 "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
538 "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v , s')"
539 "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf,x,s')"
540 "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')"
541 "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v ,x,s')"
542 "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v , s')"
543 "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
544 "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> s' " == "(s,oi,a, s') \<in> halloc G"
545 "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> (x,s')" <= "(s ,x,s') \<in> sxalloc G"
546 "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' " == "(s , s') \<in> sxalloc G"
548 inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
551 "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
553 New: "\<lbrakk>new_Addr (heap s) = Some a;
554 (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
555 else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
557 G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
559 inductive "sxalloc G" intros (* allocating exception objects for
560 standard exceptions (other than OutOfMemory) *)
562 Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s"
564 XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
566 SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
567 G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
571 *} (* dummy text command to break paragraph for latex;
572 large paragraphs exhaust memory of debian pdflatex *)
574 inductive "eval G" intros
576 (* propagation of abrupt completion *)
580 "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
583 (* execution of statements *)
586 Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
589 Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
590 G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
592 Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
593 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
595 Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
596 G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
597 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
601 If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
602 G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
603 G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
605 (* cf. 14.10, 14.10.1 *)
606 (* G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
607 (* A "continue jump" from the while body c is handled by
608 this rule. If a continue jump with the proper label was invoked inside c
609 this label (Cont l) is deleted out of the abrupt component of the state
610 before the iterative evaluation of the while statement.
611 A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
613 Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
614 if normal s1 \<and> the_Bool b
615 then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and>
616 G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
617 else s3 = s1\<rbrakk> \<Longrightarrow>
618 G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
620 Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
623 Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
624 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
627 Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
628 if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
629 G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
632 Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
633 G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
634 s3=(if (\<exists> err. x1=Some (Error err))
636 else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk>
638 G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
639 (* cf. 12.4.2, 8.5 *)
640 Init: "\<lbrakk>the (class G C) = c;
641 if inited C (globs s0) then s3 = Norm s0
642 else (G\<turnstile>Norm (init_class_obj G C s0)
643 \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
644 G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>
646 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
647 (* This class initialisation rule is a little bit inaccurate. Look at the
649 1. The current class object (the static fields) are initialised
651 2. Then the superclasses are initialised
652 3. The static initialiser of the current class is invoked
653 More precisely we should expect another ordering, namely 2 1 3.
654 But we can't just naively toggle 1 and 2. By calling init_class_obj
655 before initialising the superclasses we also implicitly record that
656 we have started to initialise the current class (by setting an
657 value for the class object). This becomes
658 crucial for the completeness proof of the axiomatic semantics
659 (AxCompl.thy). Static initialisation requires an induction on the number
660 of classes not yet initialised (or to be more precise, classes where the
661 initialisation has not yet begun).
662 So we could first assign a dummy value to the class before
663 superclass initialisation and afterwards set the correct values.
664 But as long as we don't take memory overflow into account
665 when allocating class objects, and don't model definite assignment in
666 the static initialisers, we can leave things as they are for convenience.
668 (* evaluation of expressions *)
670 (* cf. 15.8.1, 12.4.1 *)
671 NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
672 G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
673 G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
675 (* cf. 15.9.1, 12.4.1 *)
676 NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2;
677 G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
678 G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
681 Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
682 s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
683 G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
686 Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
687 b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
688 G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
691 Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
693 UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk>
694 \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
696 BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1;
697 G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
698 \<succ>\<rightarrow> (In1 v2,s2)
700 \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
703 Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
706 Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
707 G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
710 Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
711 G\<turnstile> s1 \<midarrow>e-\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow>
712 G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
715 Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
716 G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
717 G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
720 (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
722 "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
723 D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
724 s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
725 s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
726 G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
728 G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
729 (* The accessibility check is after init_lvars, to keep it simple. Init_lvars
730 already tests for the absence of a null-pointer reference in case of an
731 instance method invocation
734 Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
735 G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
736 (* The local variables l are just a dummy here. The are only used by
737 the smallstep semantics *)
738 (* cf. 14.15, 12.4.1 *)
739 Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
740 G\<turnstile>Norm s0 \<midarrow>Body D c
741 -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
742 (* The local variables l are just a dummy here. The are only used by
743 the smallstep semantics *)
744 (* evaluation of variables *)
746 (* cf. 15.13.1, 15.7.2 *)
747 LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
749 (* cf. 15.10.1, 12.4.1 *)
750 FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
751 (v,s2') = fvar statDeclC stat fn a s2;
752 s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
753 G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
754 (* The accessibility check is after fvar, to keep it simple. Fvar already
755 tests for the absence of a null-pointer reference in case of an instance
759 (* cf. 15.12.1, 15.25.1 *)
760 AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
761 (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
762 G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
765 (* evaluation of expression lists *)
769 "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
772 Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
773 G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
774 G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
776 (* Rearrangement of premisses:
777 [0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
778 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
779 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
783 bind_thm ("eval_induct_", rearrange_prems
784 [0,1,2,8,4,30,31,27,15,16,
785 17,18,19,20,21,3,5,25,26,23,6,
786 7,11,9,13,14,12,22,10,28,
787 29,24] (thm "eval.induct"))
793 *} (* dummy text command to break paragraph for latex;
794 large paragraphs exhaust memory of debian pdflatex *)
796 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
797 and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
799 s2 (* Fin *) and and s2 (* NewC *)]
801 declare split_if [split del] split_if_asm [split del]
802 option.split [split del] option.split_asm [split del]
803 inductive_cases halloc_elim_cases:
804 "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
805 "G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
807 inductive_cases sxalloc_elim_cases:
808 "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'"
809 "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
810 "G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
811 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
813 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';
814 \<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;
815 \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P
816 \<rbrakk> \<Longrightarrow> P"
818 apply (erule sxalloc_cases)
822 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
823 declare split_paired_All [simp del] split_paired_Ex [simp del]
825 simpset_ref() := simpset() delloop "split_all_tac"
827 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
829 inductive_cases eval_elim_cases:
830 "G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> vs'"
831 "G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> xs'"
832 "G\<turnstile>Norm s \<midarrow>In1r (Do j) \<succ>\<rightarrow> xs'"
833 "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<rightarrow> xs'"
834 "G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'"
835 "G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'"
836 "G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'"
837 "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<rightarrow> vs'"
838 "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<rightarrow> vs'"
839 "G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'"
840 "G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'"
841 "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'"
842 "G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> vs'"
843 "G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> vs'"
844 "G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> xs'"
845 "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> xs'"
846 "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> xs'"
847 "G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<rightarrow> xs'"
848 "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> vs'"
849 "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> xs'"
850 "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<rightarrow> xs'"
851 "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> xs'"
852 "G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> xs'"
853 "G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> vs'"
854 "G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> vs'"
855 "G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> vs'"
856 "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> xs'"
857 "G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<rightarrow> vs'"
858 "G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> vs'"
859 "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
860 "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> xs'"
861 declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)
862 declare split_paired_All [simp] split_paired_Ex [simp]
864 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
866 declare split_if [split] split_if_asm [split]
867 option.split [split] option.split_asm [split]
870 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')
871 \<Longrightarrow> case t of
872 In1 ec \<Rightarrow> (case ec of
873 Inl e \<Rightarrow> (\<exists>v. w = In1 v)
874 | Inr c \<Rightarrow> w = \<diamondsuit>)
875 | In2 e \<Rightarrow> (\<exists>v. w = In2 v)
876 | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
877 apply (erule eval_cases)
879 apply (induct_tac "t")
880 apply (induct_tac "a")
886 fun eval_fun nam inj rhs =
888 val name = "eval_" ^ nam ^ "_eq"
889 val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
890 val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
891 (K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
892 fun is_Inj (Const (inj,_) $ _) = true
894 fun pred (_ $ (Const ("Pair",_) $ _ $
895 (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
897 make_simproc name lhs pred (thm name)
900 val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
901 val eval_var_proc =eval_fun "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
902 val eval_exprs_proc=eval_fun "exprs""In3" "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
903 val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s'";
904 Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
905 bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
908 declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
910 text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
911 used in smallstep semantics, not in the bigstep semantics. So their is no
912 valid evaluation of these terms
916 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
919 assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
920 normal: "normal s" and
921 callee: "t=In1l (Callee l e)"
927 by (cases s') fastsimp
931 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
934 assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
935 normal: "normal s" and
936 callee: "t=In1l (InsInitE c e)"
942 by (cases s') fastsimp
945 lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
948 assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
949 normal: "normal s" and
950 callee: "t=In2 (InsInitV c w)"
956 by (cases s') fastsimp
959 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
962 assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
963 normal: "normal s" and
964 callee: "t=In1r (FinA a c)"
970 by (cases s') fastsimp
973 lemma eval_no_abrupt_lemma:
974 "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
975 by (erule eval_cases, auto)
977 lemma eval_no_abrupt:
978 "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') =
979 (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
981 apply (frule eval_no_abrupt_lemma, auto)+
986 fun is_None (Const ("Datatype.option.None",_)) = true
988 fun pred (t as (_ $ (Const ("Pair",_) $
989 (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
991 val eval_no_abrupt_proc =
992 make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred
993 (thm "eval_no_abrupt")
995 Addsimprocs [eval_no_abrupt_proc]
999 lemma eval_abrupt_lemma:
1000 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
1001 by (erule eval_cases, auto)
1004 " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =
1005 (s'=(Some xc,s) \<and> w=arbitrary3 t \<and>
1006 G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
1008 apply (frule eval_abrupt_lemma, auto)+
1013 fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
1015 fun pred (_ $ (Const ("Pair",_) $
1016 _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
1017 x))) $ _ ) = is_Some x
1019 val eval_abrupt_proc =
1020 make_simproc "eval_abrupt"
1021 "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
1023 Addsimprocs [eval_abrupt_proc]
1027 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
1028 apply (case_tac "s", case_tac "a = None")
1029 by (auto intro!: eval.Lit)
1031 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
1032 apply (case_tac "s", case_tac "a = None")
1033 by (auto intro!: eval.Skip)
1035 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
1036 apply (case_tac "s", case_tac "a = None")
1037 by (auto intro!: eval.Expr)
1039 lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2"
1040 apply (case_tac "s", case_tac "a = None")
1041 by (auto intro!: eval.Comp)
1044 "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
1045 G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
1046 apply (case_tac "s", case_tac "a = None")
1047 by (auto intro!: eval.Cond)
1049 lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk>
1050 \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
1051 apply (case_tac "s", case_tac "a = None")
1052 by (auto intro!: eval.If)
1054 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s'
1055 \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
1056 apply (case_tac "s", case_tac "a = None")
1057 by (auto intro!: eval.Methd)
1060 "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;
1061 D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
1062 s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
1063 s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
1064 G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4;
1065 s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>
1066 G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
1067 apply (drule eval.Call, assumption)
1068 apply (rule HOL.refl)
1073 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0
1074 else G\<turnstile>Norm (init_class_obj G C s0)
1075 \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
1076 G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>
1077 s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>
1078 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
1079 apply (rule eval.Init)
1083 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
1084 apply (case_tac "s", simp)
1085 apply (case_tac "a")
1087 apply (rule eval_Init)
1092 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
1093 apply (case_tac "s", simp)
1094 apply (case_tac "a = None")
1095 apply (auto del: eval.Abrupt intro!: eval.intros)
1099 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s"
1100 apply (erule eval_cases)
1103 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
1107 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>
1108 (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
1109 apply (erule eval.induct)
1110 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
1114 lemma halloc_xcpt [dest!]:
1115 "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
1116 apply (erule_tac halloc_elim_cases)
1120 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
1121 G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
1125 "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s')
1126 \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
1127 apply (case_tac "s")
1128 apply (case_tac "a")
1130 apply (erule eval.Methd)
1131 apply (drule eval_abrupt_lemma)
1135 lemma eval_binop_arg2_indep:
1136 "\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
1138 (simp_all add: need_second_arg_def)
1141 lemma eval_BinOp_arg2_indepI:
1142 assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
1143 no_need: "\<not> need_second_arg binop v1"
1144 shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
1145 (is "?EvalBinOp v2")
1148 have "?EvalBinOp Unit"
1149 by (rule eval.BinOp)
1153 have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
1154 by (simp add: eval_binop_arg2_indep)
1161 section "single valued"
1163 lemma unique_halloc [rule_format (no_asm)]:
1164 "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
1165 apply (simp (no_asm_simp) only: split_tupled_all)
1166 apply (erule halloc.induct)
1167 apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
1168 apply (drule trans [THEN sym], erule sym)
1170 apply (drule trans [THEN sym], erule sym)
1175 lemma single_valued_halloc:
1176 "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
1177 apply (unfold single_valued_def)
1178 by (clarsimp, drule (1) unique_halloc, auto)
1181 lemma unique_sxalloc [rule_format (no_asm)]:
1182 "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
1183 apply (simp (no_asm_simp) only: split_tupled_all)
1184 apply (erule sxalloc.induct)
1185 apply (auto dest: unique_halloc elim!: sxalloc_elim_cases
1186 split del: split_if split_if_asm)
1189 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
1190 apply (unfold single_valued_def)
1191 apply (blast dest: unique_sxalloc)
1194 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
1197 lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
1198 res=the (locals (store s2) Result);
1199 s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
1200 G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
1201 by (auto elim: eval.Body)
1203 lemma unique_eval [rule_format (no_asm)]:
1204 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
1205 apply (case_tac "ws")
1207 apply (erule thin_rl)
1208 apply (erule eval_induct)
1209 apply (tactic {* ALLGOALS (EVERY'
1210 [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
1213 apply (simp (no_asm_use) only: split add: split_if_asm)
1215 prefer 30 (* Init *)
1216 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
1217 prefer 26 (* While *)
1218 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
1219 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
1220 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
1223 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
1227 lemma single_valued_eval:
1228 "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
1229 apply (unfold single_valued_def)
1230 by (clarify, drule (1) unique_eval, auto)