12854

1 
(* Title: isabelle/Bali/Eval.thy


2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1997 Technische Universitaet Muenchen


5 
*)


6 
header {* Operational evaluation (bigstep) semantics of Java expressions and


7 
statements


8 
*}


9 


10 
theory Eval = State + DeclConcepts:


11 


12 
text {*


13 


14 
improvements over Java Specification 1.0:


15 
\begin{itemize}


16 
\item dynamic method lookup does not need to consider the return type


17 
(cf.15.11.4.4)


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


20 
(was not specified)


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


24 
rhs


25 
\item fixed exact positions of class initializations


26 
(immediate at first active use)


27 
\end{itemize}


28 


29 
design issues:


30 
\begin{itemize}


31 
\item evaluation vs. (singlestep) transition semantics


32 
evaluation semantics chosen, because:


33 
\begin{itemize}


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


39 
needed


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 metalevel


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)


46 
\end{itemize}


47 
\item unified evaluation for variables, expressions, expression lists,


48 
statements


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


53 
unique.


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.


56 
\begin{itemize}


57 
\item[++] faciliates exception handling


58 
\item[+] symmetry


59 
\end{itemize}


60 
\item the rules are defined carefully in order to be applicable even in not


61 
typecorrect situations (yielding undefined values),


62 
e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.


63 
\begin{itemize}


64 
\item[++] fewer rules


65 
\item[] less readable because of auxiliary functions like @{text the_Addr}


66 
\end{itemize}


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


70 
\begin{itemize}


71 
\item[+] no redundancy in case distinctions


72 
\end{itemize}


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


79 
the program.


80 
\begin{itemize}


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


84 
evaluation rules


85 
\end{itemize}


86 
\item unfortunately @{text new_Addr} is not directly executable because of


87 
Hilbert operator.


88 
\end{itemize}


89 
simplifications:


90 
\begin{itemize}


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


95 
modelled


96 
\item exceptions in initializations not replaced by ExceptionInInitializerError


97 
\end{itemize}


98 
*}


99 


100 
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"


101 
vals = "(val, vvar, val list) sum3"


102 
translations


103 
"vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"


104 
"vals" <= (type)"(val, vvar, val list) sum3"


105 


106 
syntax (xsymbols)


107 
dummy_res :: "vals" ("\<diamondsuit>")


108 
translations


109 
"\<diamondsuit>" == "In1 Unit"


110 


111 
constdefs


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


115 


116 
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"


117 
by (simp add: arbitrary3_def)


118 


119 
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"


120 
by (simp add: arbitrary3_def)


121 


122 
lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary"


123 
by (simp add: arbitrary3_def)


124 


125 
lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary"


126 
by (simp add: arbitrary3_def)


127 


128 


129 
section "exception throwing and catching"


130 


131 
constdefs


132 
throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt"


133 
"throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"


134 


135 
lemma throw_def2:


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))


139 
done


140 


141 
constdefs


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"


144 


145 
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"


146 
by (simp add: fits_def)


147 


148 


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)


152 


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


158 
apply simp_all


159 
apply (case_tac "T")


160 
defer


161 
apply (case_tac "a' = Null")


162 
apply simp_all


163 
done


164 


165 
constdefs


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"


169 


170 
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"


171 
apply (unfold catch_def)


172 
apply (simp (no_asm))


173 
done


174 


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))


179 
done


180 


181 
constdefs


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


185 


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))


191 
done


192 


193 


194 


195 
section "misc"


196 


197 
constdefs


198 


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


202 


203 
(*


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)


208 
*)


209 


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)


213 


214 
(*


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)


219 
*)


220 


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)


225 


226 


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)


230 


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


234 
apply auto


235 
done


236 


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


241 
apply auto


242 
done


243 


244 
(*


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


252 
apply auto


253 
done


254 
*)


255 


256 
constdefs


257 


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"


260 


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))


264 
done


265 


266 
constdefs


267 


268 
(*


269 
target :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"


270 
"target m s a' t


271 
\<equiv> if m = IntVir


272 
then obj_class (lookup_obj s a')


273 
else the_Class (RefT t)"


274 
*)


275 


276 
invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"


277 
"invocation_class m s a' statT


278 
\<equiv> (case m of


279 
Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC)


280 
then the_Class (RefT statT)


281 
else Object


282 
 SuperM \<Rightarrow> the_Class (RefT statT)


283 
 IntVir \<Rightarrow> obj_class (lookup_obj s a'))"


284 


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)


289 
sig))"


290 


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)


294 


295 
lemma dynclass_SuperM [simp]:


296 
"invocation_class SuperM s a' statT = the_Class (RefT statT)"


297 
by (simp add: invocation_class_def)


298 
(*


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)


302 
*)


303 


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)


307 
else Object)"


308 
by (simp add: invocation_class_def)


309 


310 
constdefs


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));


316 
l = \<lambda> k.


317 
(case k of


318 
EName e


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)))


323 
 This


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


326 


327 


328 


329 
lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =


330 
set_lvars


331 
(\<lambda> k.


332 
(case k of


333 
EName e


334 
\<Rightarrow> (case e of


335 
VNam v


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))))))


340 
 This


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)


345 
done


346 


347 
constdefs


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


351 


352 
lemma body_def2:


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)


356 
apply auto


357 
done


358 


359 
section "variables"


360 


361 
constdefs


362 


363 
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"


364 
"lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"


365 


366 
fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"


367 
"fvar C stat fn a' s


368 
\<equiv> let (oref,xf) = if stat then (Stat C,id)


369 
else (Heap (the_Addr a'),np a');


370 
n = Inl (fn,C);


371 
f = (\<lambda>v. supd (upd_gobj oref n v))


372 
in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"


373 


374 
avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"


375 
"avar G i' a' s


376 
\<equiv> let oref = Heap (the_Addr a');


377 
i = the_Intg i';


378 
n = Inr i;


379 
(T,k,cs) = the_Arr (globs (store s) oref);


380 
f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T)


381 
ArrStore x


382 
,upd_gobj oref n v s))


383 
in ((the (cs n),f)


384 
,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"


385 


386 
lemma fvar_def2: "fvar C stat fn a' s =


387 
((the


388 
(values


389 
(the (globs (store s) (if stat then Stat C else Heap (the_Addr a'))))


390 
(Inl (fn,C)))


391 
,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a'))


392 
(Inl (fn,C))


393 
v)))


394 
,abupd (if stat then id else np a') s)


395 
"


396 
apply (unfold fvar_def)


397 
apply (simp (no_asm) add: Let_def split_beta)


398 
done


399 


400 
lemma avar_def2: "avar G i' a' s =


401 
((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a'))))))


402 
(Inr (the_Intg i')))


403 
,(\<lambda>v (x,s'). (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)


404 
(Heap (the_Addr a'))))))


405 
ArrStore x


406 
,upd_gobj (Heap (the_Addr a'))


407 
(Inr (the_Intg i')) v s')))


408 
,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s)


409 
(Heap (the_Addr a'))))))) IndOutBound \<circ> np a')


410 
s)"


411 
apply (unfold avar_def)


412 
apply (simp (no_asm) add: Let_def split_beta)


413 
done


414 


415 


416 
section "evaluation judgments"


417 


418 
consts


419 
eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set"


420 
halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set"


421 
sxalloc:: "prog \<Rightarrow> (state \<times> state) set"


422 


423 


424 
syntax


425 
eval ::"[prog,state,term,vals*state]=>bool"("__ _>> _" [61,61,80, 61]60)


426 
exec ::"[prog,state,stmt ,state]=>bool"("__ _> _" [61,61,65, 61]60)


427 
evar ::"[prog,state,var ,vvar,state]=>bool"("__ _=>_> _"[61,61,90,61,61]60)


428 
eval_::"[prog,state,expr ,val, state]=>bool"("__ _>_> _"[61,61,80,61,61]60)


429 
evals::"[prog,state,expr list ,


430 
val list ,state]=>bool"("__ _#>_> _"[61,61,61,61,61]60)


431 
hallo::"[prog,state,obj_tag,


432 
loc,state]=>bool"("__ halloc _>_> _"[61,61,61,61,61]60)


433 
sallo::"[prog,state ,state]=>bool"("__ sxalloc> _"[61,61, 61]60)


434 


435 
syntax (xsymbols)


436 
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _" [61,61,80, 61]60)


437 
exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60)


438 
evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)


439 
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<succ>_\<rightarrow> _"[61,61,80,61,61]60)


440 
evals::"[prog,state,expr list ,


441 
val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)


442 
hallo::"[prog,state,obj_tag,


443 
loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)


444 
sallo::"[prog,state, state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61, 61]60)


445 


446 
translations


447 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> w___s' " == "(s,t,w___s') \<in> eval G"


448 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w, s')" <= "(s,t,w, s') \<in> eval G"


449 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"


450 
"G\<turnstile>s \<midarrow>c \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"


451 
"G\<turnstile>s \<midarrow>c \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit> , s')"


452 
"G\<turnstile>s \<midarrow>e\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"


453 
"G\<turnstile>s \<midarrow>e\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v , s')"


454 
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf,x,s')"


455 
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')"


456 
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v ,x,s')"


457 
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v , s')"


458 
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"


459 
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> s' " == "(s,oi,a, s') \<in> halloc G"


460 
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> (x,s')" <= "(s ,x,s') \<in> sxalloc G"


461 
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' " == "(s , s') \<in> sxalloc G"


462 


463 
inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)


464 


465 
Abrupt:


466 
"G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"


467 


468 
New: "\<lbrakk>new_Addr (heap s) = Some a;


469 
(x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)


470 
else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>


471 
\<Longrightarrow>


472 
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"


473 


474 
inductive "sxalloc G" intros (* allocating exception objects for


475 
standard exceptions (other than OutOfMemory) *)


476 


477 
Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s"


478 


479 
XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"


480 


481 
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>


482 
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"


483 


484 


485 
inductive "eval G" intros


486 


487 
(* propagation of abrupt completion *)


488 


489 
(* cf. 14.1, 15.5 *)


490 
Abrupt:


491 
"G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"


492 


493 


494 
(* execution of statements *)


495 


496 
(* cf. 14.5 *)


497 
Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"


498 


499 
(* cf. 14.7 *)


500 
Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>


501 
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"


502 


503 
Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>


504 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"


505 
(* cf. 14.2 *)


506 
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;


507 
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>


508 
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"


509 


510 


511 
(* cf. 14.8.2 *)


512 
If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1;


513 
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>


514 
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"


515 


516 
(* cf. 14.10, 14.10.1 *)


517 
(* G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)


518 
(* A "continue jump" from the while body c is handled by


519 
this rule. If a continue jump with the proper label was invoked inside c


520 
this label (Cont l) is deleted out of the abrupt component of the state


521 
before the iterative evaluation of the while statement.


522 
A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).


523 
*)


524 
Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1;


525 
if normal s1 \<and> the_Bool b


526 
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and>


527 
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)


528 
else s3 = s1\<rbrakk> \<Longrightarrow>


529 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"


530 


531 
Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"


532 


533 
(* cf. 14.16 *)


534 
Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>


535 
G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"


536 


537 
(* cf. 14.18.1 *)


538 
Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;


539 
if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>


540 
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"


541 


542 
(* cf. 14.18.2 *)


543 
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);


544 
G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>


545 
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"


546 


547 
(* cf. 12.4.2, 8.5 *)


548 
Init: "\<lbrakk>the (class G C) = c;


549 
if inited C (globs s0) then s3 = Norm s0


550 
else (G\<turnstile>Norm (init_class_obj G C s0)


551 
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>


552 
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>


553 
\<Longrightarrow>


554 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"


555 


556 
(* evaluation of expressions *)


557 


558 
(* cf. 15.8.1, 12.4.1 *)


559 
NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;


560 
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>


561 
G\<turnstile>Norm s0 \<midarrow>NewC C\<succ>Addr a\<rightarrow> s2"


562 


563 
(* cf. 15.9.1, 12.4.1 *)


564 
NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>i'\<rightarrow> s2;


565 
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>


566 
G\<turnstile>Norm s0 \<midarrow>New T[e]\<succ>Addr a\<rightarrow> s3"


567 


568 
(* cf. 15.15 *)


569 
Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1;


570 
s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>


571 
G\<turnstile>Norm s0 \<midarrow>Cast T e\<succ>v\<rightarrow> s2"


572 


573 
(* cf. 15.19.2 *)


574 
Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1;


575 
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>


576 
G\<turnstile>Norm s0 \<midarrow>e InstOf T\<succ>Bool b\<rightarrow> s1"


577 


578 
(* cf. 15.7.1 *)


579 
Lit: "G\<turnstile>Norm s \<midarrow>Lit v\<succ>v\<rightarrow> Norm s"


580 


581 


582 


583 
(* cf. 15.10.2 *)


584 
Super: "G\<turnstile>Norm s \<midarrow>Super\<succ>val_this s\<rightarrow> Norm s"


585 


586 
(* cf. 15.2 *)


587 
Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>


588 
G\<turnstile>Norm s0 \<midarrow>Acc va\<succ>v\<rightarrow> s1"


589 


590 
(* cf. 15.25.1 *)


591 
Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;


592 
G\<turnstile> s1 \<midarrow>e\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow>


593 
G\<turnstile>Norm s0 \<midarrow>va:=e\<succ>v\<rightarrow> assign f v s2"


594 


595 
(* cf. 15.24 *)


596 
Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0\<succ>b\<rightarrow> s1;


597 
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>


598 
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2\<succ>v\<rightarrow> s2"


599 


600 


601 
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)


602 
Call:


603 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;


604 
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;


605 
G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2


606 
\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ>v\<rightarrow> s3\<rbrakk>


607 
\<Longrightarrow>


608 
G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)\<succ>v\<rightarrow> (restore_lvars s2 s3)"


609 


610 
Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>


611 
G\<turnstile>Norm s0 \<midarrow>Methd D sig\<succ>v\<rightarrow> s1"


612 


613 
(* cf. 14.15, 12.4.1 *)


614 
Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>


615 
G\<turnstile>Norm s0 \<midarrow>Body D c \<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"


616 


617 
(* evaluation of variables *)


618 


619 
(* cf. 15.13.1, 15.7.2 *)


620 
LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"


621 


622 
(* cf. 15.10.1, 12.4.1 *)


623 
FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>a\<rightarrow> s2;


624 
(v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>


625 
G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"


626 


627 
(* cf. 15.12.1, 15.25.1 *)


628 
AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2\<succ>i\<rightarrow> s2;


629 
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>


630 
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"


631 


632 


633 
(* evaluation of expression lists *)


634 


635 
(* cf. 15.11.4.2 *)


636 
Nil:


637 
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"


638 


639 
(* cf. 15.6.4 *)


640 
Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e \<succ> v \<rightarrow> s1;


641 
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>


642 
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"


643 


644 
(* Rearrangement of premisses:


645 
[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),


646 
17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),


647 
7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),


648 
27(AVar),22(Call)]


649 
*)


650 
ML {*


651 
bind_thm ("eval_induct_", rearrange_prems


652 
[0,1,2,8,4,28,29,25,15,16,


653 
17,18,19,3,5,23,24,21,6,


654 
7,11,9,13,14,12,20,10,26,


655 
27,22] (thm "eval.induct"))


656 
*}


657 


658 
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and


659 
and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and


660 
s2 (* Fin *) and and s2 (* NewC *)]


661 


662 
declare split_if [split del] split_if_asm [split del]


663 
option.split [split del] option.split_asm [split del]


664 
inductive_cases halloc_elim_cases:


665 
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"


666 
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"


667 


668 
inductive_cases sxalloc_elim_cases:


669 
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'"


670 
"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"


671 
"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"


672 
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"


673 


674 
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';


675 
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;


676 
\<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P


677 
\<rbrakk> \<Longrightarrow> P"


678 
apply cut_tac


679 
apply (erule sxalloc_cases)


680 
apply blast+


681 
done


682 


683 
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)


684 
declare split_paired_All [simp del] split_paired_Ex [simp del]


685 
ML_setup {*


686 
simpset_ref() := simpset() delloop "split_all_tac"


687 
*}


688 
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"


689 


690 
inductive_cases eval_elim_cases:


691 
"G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> vs'"


692 
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> xs'"


693 
"G\<turnstile>Norm s \<midarrow>In1r (Do j) \<succ>\<rightarrow> xs'"


694 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<rightarrow> xs'"


695 
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'"


696 
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'"


697 
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'"


698 
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'"


699 
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'"


700 
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'"


701 
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> vs'"


702 
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> vs'"


703 
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> xs'"


704 
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> xs'"


705 
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> xs'"


706 
"G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<rightarrow> xs'"


707 
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> vs'"


708 
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> xs'"


709 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<rightarrow> xs'"


710 
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> xs'"


711 
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> xs'"


712 
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> vs'"


713 
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> vs'"


714 
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> vs'"


715 
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> xs'"


716 
"G\<turnstile>Norm s \<midarrow>In2 ({C,stat}e..fn) \<succ>\<rightarrow> vs'"


717 
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> vs'"


718 
"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"


719 
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> xs'"


720 
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)


721 
declare split_paired_All [simp] split_paired_Ex [simp]


722 
ML_setup {*


723 
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)


724 
*}


725 
declare split_if [split] split_if_asm [split]


726 
option.split [split] option.split_asm [split]


727 


728 
lemma eval_Inj_elim:


729 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')


730 
\<Longrightarrow> case t of


731 
In1 ec \<Rightarrow> (case ec of


732 
Inl e \<Rightarrow> (\<exists>v. w = In1 v)


733 
 Inr c \<Rightarrow> w = \<diamondsuit>)


734 
 In2 e \<Rightarrow> (\<exists>v. w = In2 v)


735 
 In3 e \<Rightarrow> (\<exists>v. w = In3 v)"


736 
apply (erule eval_cases)


737 
apply auto


738 
apply (induct_tac "t")


739 
apply (induct_tac "a")


740 
apply auto


741 
done


742 


743 
ML_setup {*


744 
fun eval_fun nam inj rhs =


745 
let


746 
val name = "eval_" ^ nam ^ "_eq"


747 
val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"


748 
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")


749 
(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])


750 
fun is_Inj (Const (inj,_) $ _) = true


751 
 is_Inj _ = false


752 
fun pred (_ $ (Const ("Pair",_) $ _ $


753 
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x


754 
in


755 
make_simproc name lhs pred (thm name)


756 
end


757 


758 
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t\<succ>v \<rightarrow> s'"


759 
val eval_var_proc =eval_fun "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"


760 
val eval_exprs_proc=eval_fun "exprs""In3" "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"


761 
val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s'";


762 
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];


763 
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))


764 
*}


765 


766 
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]


767 


768 


769 
lemma eval_no_abrupt_lemma:


770 
"\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"


771 
by (erule eval_cases, auto)


772 


773 
lemma eval_no_abrupt:


774 
"G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') =


775 
(x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"


776 
apply auto


777 
apply (frule eval_no_abrupt_lemma, auto)+


778 
done


779 


780 
ML {*


781 
local


782 
fun is_None (Const ("Option.option.None",_)) = true


783 
 is_None _ = false


784 
fun pred (t as (_ $ (Const ("Pair",_) $


785 
(Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x


786 
in


787 
val eval_no_abrupt_proc =


788 
make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred


789 
(thm "eval_no_abrupt")


790 
end;


791 
Addsimprocs [eval_no_abrupt_proc]


792 
*}


793 


794 


795 
lemma eval_abrupt_lemma:


796 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"


797 
by (erule eval_cases, auto)


798 


799 
lemma eval_abrupt:


800 
" G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =


801 
(s'=(Some xc,s) \<and> w=arbitrary3 t \<and>


802 
G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"


803 
apply auto


804 
apply (frule eval_abrupt_lemma, auto)+


805 
done


806 


807 
ML {*


808 
local


809 
fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true


810 
 is_Some _ = false


811 
fun pred (_ $ (Const ("Pair",_) $


812 
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $


813 
x))) $ _ ) = is_Some x


814 
in


815 
val eval_abrupt_proc =


816 
make_simproc "eval_abrupt"


817 
"G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")


818 
end;


819 
Addsimprocs [eval_abrupt_proc]


820 
*}


821 


822 


823 
lemma LitI: "G\<turnstile>s \<midarrow>Lit v\<succ>(if normal s then v else arbitrary)\<rightarrow> s"


824 
apply (case_tac "s", case_tac "a = None")


825 
by (auto intro!: eval.Lit)


826 


827 
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"


828 
apply (case_tac "s", case_tac "a = None")


829 
by (auto intro!: eval.Skip)


830 


831 
lemma ExprI: "G\<turnstile>s \<midarrow>e\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"


832 
apply (case_tac "s", case_tac "a = None")


833 
by (auto intro!: eval.Expr)


834 


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


836 
apply (case_tac "s", case_tac "a = None")


837 
by (auto intro!: eval.Comp)


838 


839 
lemma CondI:


840 
"\<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>


841 
G\<turnstile>s \<midarrow>e ? e1 : e2\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"


842 
apply (case_tac "s", case_tac "a = None")


843 
by (auto intro!: eval.Cond)


844 


845 
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>


846 
\<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"


847 
apply (case_tac "s", case_tac "a = None")


848 
by (auto intro!: eval.If)


849 


850 
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig\<succ>v\<rightarrow> s'"


851 
apply (case_tac "s", case_tac "a = None")


852 
by (auto intro!: eval.Methd)


853 


854 
lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;


855 
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;


856 
G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2


857 
\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ> v\<rightarrow> s3;


858 
s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>


859 
G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}ps)\<succ>v\<rightarrow> s3'"


860 
apply (drule eval.Call, assumption)


861 
apply (rule HOL.refl)


862 
apply simp+


863 
done


864 


865 
lemma eval_Init:


866 
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0


867 
else G\<turnstile>Norm (init_class_obj G C s0)


868 
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>


869 
G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>


870 
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>


871 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"


872 
apply (rule eval.Init)


873 
apply auto


874 
done


875 


876 
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"


877 
apply (case_tac "s", simp)


878 
apply (case_tac "a")


879 
apply safe


880 
apply (rule eval_Init)


881 
apply auto


882 
done


883 


884 
lemma eval_StatRef:


885 
"G\<turnstile>s \<midarrow>StatRef rt\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"


886 
apply (case_tac "s", simp)


887 
apply (case_tac "a = None")


888 
apply (auto del: eval.Abrupt intro!: eval.intros)


889 
done


890 


891 


892 
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s"


893 
apply (erule eval_cases)


894 
by auto


895 


896 
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"


897 
by auto


898 


899 
(*unused*)


900 
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>


901 
(\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"


902 
apply (erule eval.induct)


903 
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+


904 
apply auto


905 
done


906 


907 
lemma halloc_xcpt [dest!]:


908 
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"


909 
apply (erule_tac halloc_elim_cases)


910 
by auto


911 


912 
(*


913 
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"


914 
G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"


915 
*)


916 


917 
lemma eval_Methd:


918 
"G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"


919 
apply (case_tac "s")


920 
apply (case_tac "a")


921 
apply clarsimp+


922 
apply (erule eval.Methd)


923 
apply (drule eval_abrupt_lemma)


924 
apply force


925 
done


926 


927 


928 
section "single valued"


929 


930 
lemma unique_halloc [rule_format (no_asm)]:


931 
"\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"


932 
apply (simp (no_asm_simp) only: split_tupled_all)


933 
apply (erule halloc.induct)


934 
apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm)


935 
apply (drule trans [THEN sym], erule sym)


936 
defer


937 
apply (drule trans [THEN sym], erule sym)


938 
apply auto


939 
done


940 


941 


942 
lemma single_valued_halloc:


943 
"single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"


944 
apply (unfold single_valued_def)


945 
by (clarsimp, drule (1) unique_halloc, auto)


946 


947 


948 
lemma unique_sxalloc [rule_format (no_asm)]:


949 
"\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"


950 
apply (simp (no_asm_simp) only: split_tupled_all)


951 
apply (erule sxalloc.induct)


952 
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases


953 
split del: split_if split_if_asm)


954 
done


955 


956 
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"


957 
apply (unfold single_valued_def)


958 
apply (blast dest: unique_sxalloc)


959 
done


960 


961 
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"


962 
by auto


963 


964 
lemma unique_eval [rule_format (no_asm)]:


965 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"


966 
apply (case_tac "ws")


967 
apply (simp only:)


968 
apply (erule thin_rl)


969 
apply (erule eval_induct)


970 
apply (tactic {* ALLGOALS (EVERY'


971 
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})


972 
(* 29 subgoals *)


973 
prefer 26 (* Try *)


974 
apply (simp (no_asm_use) only: split add: split_if_asm)


975 
(* 32 subgoals *)


976 
prefer 28 (* Init *)


977 
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)


978 
prefer 24 (* While *)


979 
apply (simp (no_asm_use) only: split add: split_if_asm, blast)


980 
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)


981 
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)


982 
apply blast


983 
(* 31 subgoals *)


984 
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+


985 
done


986 


987 
(* unused *)


988 
lemma single_valued_eval:


989 
"single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"


990 
apply (unfold single_valued_def)


991 
by (clarify, drule (1) unique_eval, auto)


992 


993 
end
