Up to index of Isabelle/Bali5
theory Eval = State:(* Title: isabelle/Bali/Eval.thy
ID: $Id: Eval.thy,v 1.88 2001/05/11 14:41:57 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of Java expressions and statements
improvements over Java Specification 1.0:
* dynamic method lookup does not need to consider the return type (cf.15.11.4.4)
* throw raises a NullPointer exception if a null reference is given, and each
throw of a standard exception yield a fresh exception object (was not specified)
* if there is not enough memory even to allocate an OutOfMemory exception,
evaluation/execution fails, i.e. simply stops (was not specified)
* array assignment checks lhs (and may throw exceptions) before evaluating rhs
* fixed exact positions of class initializations (immediate at first active use)
design issues:
* evaluation vs. (single-step) transition semantics
evaluation semantics chosen, because:
++ less verbose and therefore easier to read (and to handle in proofs)
+ more abstract
+ intermediate values (appearing in recursive rules) need not be stored
explicitly, e.g. no call body construct or stack of invocation frames
containing local variables and return addresses for method calls needed
+ convenient rule induction for subject reduction theorem
- no interleaving (for parallelism) can be described
- stating a property of infinite executions requires the meta-level argument
that this property holds for any finite prefixes of it (e.g. stopped using
a counter that is decremented to zero and then throwing an exception)
* unified evaluation for variables, expressions, expression lists, statements
* the value entry in statement rules is redundant
* the value entry in rules is irrelevant in case of exceptions, but its full
inclusion helps to make the rule structure independent of exception occurence.
* as irrelevant value entries are ignored, it does not matter if they are unique
For simplicity, (fixed) arbitrary values are preferred over "free" values.
* the rule format is such that the start state may contain an exception.
++ faciliates exception handling
+ symmetry
* the rules are defined carefully in order to be applicable even in not
type-correct situations (yielding undefined values),
e.g. the_Addr (Val (Bool b)) = arbitrary.
++ fewer rules
- less readable because of auxiliary functions like the_Addr
Alternative: "defensive" evaluation throwing some InternalError exception
in case of (impossible, for correct programs) type mismatches
* there is exactly one rule per syntactic construct
+ no redundancy in case distinctions
* halloc fails iff there is no free heap address. When there is
only one free heap address left, it returns an OutOfMemory exception.
In this way it is guaranteed that when an OutOfMemory exception is thrown for
the first time, there is a free location on the heap to allocate it.
* the allocation of objects that represent standard exceptions is deferred until
execution of any enclosing catch clause, which is transparent to the program.
- requires an auxiliary execution relation
++ avoids copies of allocation code and awkward case distinctions (whether
there is enough memory to allocate the exception) in evaluation rules
* unfortunately new_Addr is not directly executable because of Hilbert operator.
simplifications:
* local variables are initialized with default values (no definite assignment)
* garbage collection not considered, therefore also no finalizers
* stack overflow and memory overflow during class initialization not modelled
* exceptions in initializations not replaced by ExceptionInInitializerError
*)
theory Eval = State:
types vvar = "val × (val \<Rightarrow> state \<Rightarrow> state)"
vals = "(val, vvar, val list) sum3"
translations
"vvar" <= (type) "val × (val \<Rightarrow> state \<Rightarrow> state)"
"vals" <= (type)"(val, vvar, val list) sum3"
syntax (xsymbols)
dummy_res :: "vals" ("\<bullet>")
translations
"\<bullet>" == "In1 Unit"
constdefs
arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
"arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
(\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
by (simp add: arbitrary3_def)
lemma [simp]: "arbitrary3 (In1r x) = \<bullet>"
by (simp add: arbitrary3_def)
lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary"
by (simp add: arbitrary3_def)
lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary"
by (simp add: arbitrary3_def)
section "exception throwing and catching"
constdefs
throw :: "val \<Rightarrow> xopt \<Rightarrow> xopt"
"throw a' x \<equiv> xcpt_if True (Some (XcptLoc (the_Addr a'))) (np a' x)"
lemma throw_def2:
"throw a' x = xcpt_if True (Some (XcptLoc (the_Addr a'))) (np a' x)"
apply (unfold throw_def)
apply (simp (no_asm))
done
constdefs
fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
"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"
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
by (simp add: fits_def)
lemma fits_Addr_RefT [simp]:
"G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
by (simp add: fits_def)
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>
(\<exists>t. T = RefT t) \<and> a' = Null \<or>
(\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and> G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
apply (unfold fits_def)
apply (case_tac "\<exists>pt. T = PrimT pt")
apply simp_all
apply (case_tac "T")
defer
apply (case_tac "a' = Null")
apply simp_all
done
constdefs
catch ::"prog \<Rightarrow> state \<Rightarrow> tname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60)
"G,s\<turnstile>catch C\<equiv>\<exists>xc. fst s=Some xc \<and> G,snd s\<turnstile>Addr (the_XcptLoc xc) fits Class C"
lemma catch_Norm [simp]: "¬G,Norm s\<turnstile>catch tn"
apply (unfold catch_def)
apply (simp (no_asm))
done
lemma catch_XcptLoc [simp]: "G,(Some (XcptLoc a), s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
apply (unfold catch_def)
apply (simp (no_asm))
done
constdefs
new_xcpt_var :: "ename \<Rightarrow> state \<Rightarrow> state"
"new_xcpt_var vn \<equiv> \<lambda>(x,s). Norm(lupd(EName vn\<mapsto>Addr (the_XcptLoc (the x))) s)"
lemma new_xcpt_var_def2 [simp]:
"new_xcpt_var vn (x,s) = Norm (lupd(EName vn\<mapsto>Addr (the_XcptLoc (the x))) s)"
apply (unfold new_xcpt_var_def)
apply (simp (no_asm))
done
section "misc"
constdefs
assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state"
"assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
in (x',if x' = None then s' else s)"
lemma assign_Norm_Norm [simp]:
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
by (simp add: assign_def Let_def)
lemma assign_Norm_Some [simp]:
"\<lbrakk>fst (f v (Norm s)) = Some y\<rbrakk> \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
by (simp add: assign_def Let_def split_beta)
lemma assign_Some [simp]: "assign f v (Some x,s) = (Some x,s)"
by (simp add: assign_def Let_def split_beta)
lemma assign_supd [simp]:
"assign (\<lambda>v. supd (f v)) v (x, s) = (x, if x = None then f v s else s)"
by auto
lemma assign_raise_if [simp]:
"assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =
(raise_if (b s v) xcpt x, if x=None \<and> ¬b s v then f v s else s)"
apply (case_tac "x = None")
apply auto
done
constdefs
init_comp_ty :: "ty \<Rightarrow> stmt"
"init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then init (the_Class T) else Skip"
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
apply (unfold init_comp_ty_def)
apply (simp (no_asm))
done
constdefs
target :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> tname"
"target m s a' t \<equiv> if m = IntVir
then obj_class (lookup_obj s a') else the_Class (RefT t)"
lemma target_IntVir [simp]:
"target IntVir s a' t = obj_class (lookup_obj s a')"
apply (unfold target_def)
apply (simp (no_asm))
done
lemma target_notIntVir: "m \<noteq> IntVir \<Longrightarrow> target m s a' t = the_Class (RefT t)"
apply (unfold target_def)
apply (simp (no_asm_simp))
done
lemma target_Static [simp]: "target Static s a' t = the_Class (RefT t)"
apply (unfold target_def)
apply (simp (no_asm))
done
lemma target_SuperM [simp]: "target SuperM s a' t = the_Class (RefT t)"
apply (unfold target_def)
apply (simp (no_asm))
done
constdefs
init_lvars :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
state \<Rightarrow> state"
"init_lvars G C sig mode a' pvs \<equiv> \<lambda>(x,s). let
(_,(_,pns,_),lvars,_) = the (cmethd G C sig);
l = init_vals(table_of lvars)(pns[\<mapsto>]pvs) (+)
(if mode=Static then empty else empty(()\<mapsto>a'))
in set_lvars l (if mode = Static then x else np a' x,s)"
lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =
set_lvars (init_vals(table_of (fst (snd (snd( the (cmethd G C sig))))))(fst (snd (fst (snd (the (cmethd G C sig)))))[\<mapsto>]pvs) (+)
(if mode=Static then empty else empty(()\<mapsto>a')))
(if mode=Static then x else np a' x, s)"
apply (unfold init_lvars_def)
apply (simp (no_asm) add: Let_def split_beta)
done
constdefs
body :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> expr"
"body G C sig \<equiv> let (D, _, _, c, e) = the (cmethd G C sig) in Body D c e"
lemma body_def2:
"body G C sig = (\<lambda> (D, x1, x2, c, ee). Body D c ee) (the (cmethd G C sig))"
apply (unfold body_def Let_def)
apply auto
done
section "variables"
constdefs
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
"lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
fvar :: "tname \<Rightarrow> bool \<Rightarrow> ename \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar × state"
"fvar C stat fn a' s \<equiv> let (oref,xf) = if stat then (Stat C,id)
else (Heap (the_Addr a'),np a');
n = Inl (fn,C); f = (\<lambda>v. supd (upd_gobj oref n v)) in
((the (snd (the (globs (snd s) oref)) n),f),xupd xf s)"
avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar × state"
"avar G i' a' s \<equiv> let oref = Heap (the_Addr a'); i = the_Intg i'; n = Inr i;
(T,k,cs) = the_Arr (globs (snd s) oref); f = (\<lambda>v (x,s).
(raise_if (¬G,s\<turnstile>v fits T) ArrStore x, upd_gobj oref n v s)) in
((the (cs n),f), xupd (raise_if (¬i in_bounds k) IndOutBound \<circ> np a') s)"
lemma fvar_def2: "fvar C stat fn a' s =
((the (snd (the (globs(snd s) (if stat then Stat C else (Heap(the_Addr a')))))
(Inl (fn,C))),(\<lambda>v. supd (upd_gobj (if stat then Stat C else
(Heap (the_Addr a'))) (Inl (fn,C)) v))),xupd (if stat then id else np a') s)"
apply (unfold fvar_def)
apply (simp (no_asm) add: Let_def split_beta)
done
lemma avar_def2: "avar G i' a' s =
((the(snd(snd(the_Arr(globs (snd s)(Heap(the_Addr a'))))) (Inr(the_Intg i'))),
(\<lambda>v (x,s').
(raise_if (¬G,s'\<turnstile>v fits(fst(the_Arr(globs (snd s)(Heap(the_Addr a'))))))
ArrStore x,
upd_gobj (Heap (the_Addr a')) (Inr (the_Intg i')) v s')
)),
xupd (raise_if (¬ the_Intg i' in_bounds
fst(snd((the_Arr(globs (snd s) (Heap (the_Addr a'))))))) IndOutBound
\<circ> np a') s)"
apply (unfold avar_def)
apply (simp (no_asm) add: Let_def split_beta)
done
section "evaluation judgments"
consts
eval :: "prog \<Rightarrow> (state × term × vals × state) set"
halloc:: "prog \<Rightarrow> (state × obj_tag × loc × state) set"
sxalloc:: "prog \<Rightarrow> (state × state) set"
syntax
eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _" [61,61,80, 61]60)
exec ::"[prog,state,stmt ,state]=>bool"("_|-_ -_-> _" [61,61,65, 61]60)
evar ::"[prog,state,var ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
evals::"[prog,state,expr list ,
val list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
hallo::"[prog,state,obj_tag,
loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
sallo::"[prog,state ,state]=>bool"("_|-_ -sxalloc-> _"[61,61, 61]60)
syntax (xsymbols)
eval ::"[prog,state,term,vals×state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _" [61,61,80, 61]60)
exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60)
evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
evals::"[prog,state,expr list ,
val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
hallo::"[prog,state,obj_tag,
loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
sallo::"[prog,state, state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61, 61]60)
translations
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> w___s' " == "(s,t,w___s') \<in> eval G"
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w, s')" <= "(s,t,w, s') \<in> eval G"
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
"G\<turnstile>s \<midarrow>c \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<bullet> ,x,s')"
"G\<turnstile>s \<midarrow>c \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<bullet> , s')"
"G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
"G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v , s')"
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf,x,s')"
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')"
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v ,x,s')"
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v , s')"
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> s' " == "(s,oi,a, s') \<in> halloc G"
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> (x,s')" <= "(s ,x,s') \<in> sxalloc G"
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' " == "(s , s') \<in> sxalloc G"
inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
Xcpt: "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
New: "\<lbrakk>new_Addr (heap s) = Some a;
(x,oi') = (if atleast_free (heap s) 2 then (None,oi)
else (Some (XcptLoc a),CInst (SXcpt OutOfMemory)))\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
inductive "sxalloc G" intros (* allocating exception objects for
standard exceptions (other than OutOfMemory) *)
Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s"
XcptL: "G\<turnstile>(Some (XcptLoc a ),s) \<midarrow>sxalloc\<rightarrow> (Some (XcptLoc a),s)"
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
G\<turnstile>(Some (StdXcpt xn),s0) \<midarrow>sxalloc\<rightarrow> (Some (XcptLoc a),s1)"
inductive "eval G" intros
(* propagation of exceptions *)
(* cf. 14.1, 15.5 *)
Xcpt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
(* execution of statements *)
(* cf. 14.5 *)
Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
(* cf. 14.7 *)
Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
(* cf. 14.2 *)
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
(* cf. 14.8.2 *)
If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
(* cf. 14.10, 14.10.1 *)
(* G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
if the_Bool b then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> G\<turnstile>s2 \<midarrow>While(e) c\<rightarrow> s3)
else s3 = s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>While(e) c\<rightarrow> s3"
(* cf. 14.16 *)
Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> xupd (throw a') s1"
(* cf. 14.18.1 *)
Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
(* cf. 14.18.2 *)
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> xupd (xcpt_if (x1\<noteq>None) x1) s2"
(* cf. 12.4.2, 8.5 *)
Init: "\<lbrakk>the (class G C) = (sc,si,fs,ms,ini);
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else init sc)\<rightarrow> s1 \<and>
G\<turnstile>set_lvars empty s1 \<midarrow>ini\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> s3"
(* evaluation of expressions *)
(* cf. 15.8.1, 12.4.1 *)
NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
(* cf. 15.9.1, 12.4.1 *)
NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2;
G\<turnstile>xupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
(* cf. 15.15 *)
Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
s2 = xupd (raise_if (¬G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
(* cf. 15.19.2 *)
Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
b = (v\<noteq>Null \<and> G,snd s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
(* cf. 15.7.1 *)
Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
(* cf. 15.10.2 *)
Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
(* cf. 15.2 *)
Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
(* cf. 15.25.1 *)
Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>e-\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
(* cf. 15.24 *)
Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
C = target mode (snd s2) a' cT;
G\<turnstile>init_lvars G C (mn,pTs) mode a' vs s2 \<midarrow>Methd C (mn,pTs)-\<succ>v\<rightarrow> s3\<rbrakk>\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{t,cT,mode}e..mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s3)"
Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G C sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Methd C sig-\<succ>v\<rightarrow> s1"
(* cf. 14.15, 12.4.1 *)
Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; G\<turnstile>s2 \<midarrow>e-\<succ>v\<rightarrow> s3\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Body D c e-\<succ>v\<rightarrow> s3"
(* evaluation of variables *)
(* cf. 15.13.1, 15.7.2 *)
LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
(* cf. 15.10.1, 12.4.1 *)
FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
(v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"
(* cf. 15.12.1, 15.25.1 *)
AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
(* evaluation of expression lists *)
(* cf. 15.11.4.2 *)
Nil:
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
(* cf. 15.6.4 *)
Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
(* Rearrangement of premisses:
[0,1(Xcpt),2(Skip),26(Nil),27(Cons),23(LVar),13(Cast),14(Inst),15(Lit),
16(Super),17(Acc),3(Expr),4(Comp),21(Methd),22(Body),19(Cond),5(If),6(Loop),
9(Fin),7(Throw),11(NewC),12(NewA),10(Init),18(Ass),8(Try),24(FVar),25(AVar),
20(Call)]
*)
ML {*
bind_thm ("eval_induct_", rearrange_prems
[0,1,2,26,27,23,13,14,15,
16,17,3,4,21,22,19,5,6,
9,7,11,12,10,18,8,24,25,
20] (thm "eval.induct"))
*}
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
and and s1 s2 and and s2 and and and and and and s2 and and s2 s3]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
inductive_cases halloc_elim_cases:
"G\<turnstile>(Some xc, s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
inductive_cases sxalloc_elim_cases:
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (XcptLoc a ),s) \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (StdXcpt xn),s) \<midarrow>sxalloc\<rightarrow> s'"
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;
\<And>a s. \<lbrakk>s' = (Some (XcptLoc a), s)\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
apply cut_tac
apply (erule sxalloc_cases)
apply blast+
done
declare not_None_eq [simp del] IntDef.Zero_def [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
simpset_ref() := simpset() delloop "split_all_tac"
*}
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
inductive_cases eval_elim_cases:
"G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1l (Body D c e) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1r (While(e) c) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In2 ({C,stat}e..fn) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l ({t,cT,mode}e..mn({pT}p)) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r (init C) \<succ>\<rightarrow> xs'"
declare not_None_eq [simp] IntDef.Zero_def [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
*}
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
lemma eval_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<bullet>)
| In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
apply (erule eval_cases)
apply auto
apply (induct_tac "t")
apply (induct_tac "a")
apply auto
done
ML_setup {*
fun eval_fun nam inj rhs =
let
val name = "eval_" ^ nam ^ "_eq"
val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
fun is_Inj (Const (inj,_) $ _) = true
| is_Inj _ = false
fun pred (_ $ (Const ("Pair",_) $ _ $
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
in
make_simproc name lhs pred (thm name)
end
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
val eval_var_proc =eval_fun "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
val eval_exprs_proc=eval_fun "exprs""In3" "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\<bullet> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s'";
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
bind_thms ("XcptIs", sum3_instantiate (thm "eval.Xcpt"))
*}
declare halloc.Xcpt [intro!] eval.Xcpt [intro!] XcptIs [intro!]
lemma eval_no_xcpt_lemma: "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
by (erule eval_cases, auto)
lemma eval_no_xcpt:
"G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
apply auto
apply (frule eval_no_xcpt_lemma, auto)+
done
ML {*
local
fun is_None (Const ("Option.option.None",_)) = true
| is_None _ = false
fun pred (t as (_ $ (Const ("Pair",_) $
(Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
in
val eval_no_xcpt_proc =
make_simproc "eval_no_xcpt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred
(thm "eval_no_xcpt")
end;
Addsimprocs [eval_no_xcpt_proc]
*}
lemma eval_xcpt_lemma:
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> fst s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
by (erule eval_cases, auto)
lemma eval_xcpt: "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =
(s'=(Some xc,s) \<and> w=arbitrary3 t \<and>
G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
apply auto
apply (frule eval_xcpt_lemma, auto)+
done
ML {*
local
fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
| is_Some _ = false
fun pred (_ $ (Const ("Pair",_) $
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
x))) $ _ ) = is_Some x
in
val eval_xcpt_proc =
make_simproc "eval_xcpt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_xcpt")
end;
Addsimprocs [eval_xcpt_proc]
*}
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Lit)
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Skip)
lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Expr)
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"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Comp)
lemma CondI:
"\<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>
G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Cond)
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>
\<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.If)
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'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Methd)
lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;
C = target mode (snd s2) a' cT;
G\<turnstile>init_lvars G C (mn,pTs) mode a' pvs s2 \<midarrow>Methd C (mn,pTs)-\<succ> v\<rightarrow> s3;
s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{t,cT,mode}e..mn({pTs}ps)-\<succ>v\<rightarrow> s3'"
apply (drule eval.Call, assumption)
apply (rule HOL.refl)
apply simp+
done
lemma eval_Init: "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 else
G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else init (fst (the (class G C))))\<rightarrow> s1 \<and>
G\<turnstile>set_lvars empty s1 \<midarrow>(snd (snd (snd (snd (the (class G C))))))\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> s3"
apply (rule surjective_pairing5 [THEN eval.Init])
apply auto
done
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>init C\<rightarrow> s"
apply (case_tac "s", simp)
apply (case_tac "a")
apply safe
apply (rule eval_Init)
apply auto
done
lemma eval_StatRef:
"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if fst s=None then Null else arbitrary)\<rightarrow> s"
apply (case_tac "s", simp)
apply (case_tac "a = None")
apply (auto del: eval.Xcpt intro!: eval.intros)
done
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s"
apply (erule eval_cases)
by auto
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
by auto
(*unused*)
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>
(\<forall>C. t=In1r (init C) \<longrightarrow> locals (snd s) = locals (snd s'))"
apply (erule eval.induct)
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
apply auto
done
lemma halloc_xcpt [dest!]:
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
apply (erule_tac halloc_elim_cases)
by auto
(*
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
*)
lemma eval_Methd:
"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')"
apply (case_tac "s")
apply (case_tac "a")
apply clarsimp+
apply (erule eval.Methd)
apply (drule eval_xcpt_lemma)
apply force
done
section "single_valued"
lemma unique_halloc [rule_format (no_asm)]:
"\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule halloc.induct)
apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
apply (drule trans [THEN sym], erule sym)
defer
apply (drule trans [THEN sym], erule sym)
apply auto
done
lemma single_valued_halloc:
"single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
apply (unfold single_valued_def)
by (clarsimp, drule (1) unique_halloc, auto)
lemma unique_sxalloc [rule_format (no_asm)]:
"\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule sxalloc.induct)
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases
split del: split_if split_if_asm)
done
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
apply (unfold single_valued_def)
apply (blast dest: unique_sxalloc)
done
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
by auto
lemma unique_eval [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
apply (case_tac "ws")
apply (simp only:)
apply (erule thin_rl)
apply (erule eval_induct)
apply (tactic {* ALLGOALS (EVERY'
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
(* 27 subgoals *)
prefer 24 (* Try *)
apply (simp (no_asm_use) only: split add: split_if_asm)
prefer 26 (* Init *)
apply (drule (1) trans [OF sym])
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
prefer 22 (* While *)
apply (simp (no_asm_use) only: split add: split_if_asm)
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
done
(* unused *)
lemma single_valued_eval:
"single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
apply (unfold single_valued_def)
by (clarify, drule (1) unique_eval, auto)
end
lemma
arbitrary3 (In1l x) = In1 arbitrary
lemma
arbitrary3 (In1r x) = dummy_res
lemma
arbitrary3 (In2 x) = In2 arbitrary
lemma
arbitrary3 (In3 x) = In3 arbitrary
lemma throw_def2:
throw a' x = xcpt_if True (Some (XcptLoc (the_Addr a'))) ((np a') x)
lemma fits_Null:
G,s\<turnstile>Null fits T
lemma fits_Addr_RefT:
G,s\<turnstile>Addr a fits RefT t = G|-obj_ty (the (heap s a))<=:RefT t
lemma fitsD:
G,s\<turnstile>a' fits T
==> (EX pt. T = PrimT pt) |
(EX t. T = RefT t) & a' = Null |
(EX t. T = RefT t) & a' ~= Null & G|-obj_ty (lookup_obj s a')<=:T
lemma catch_Norm:
¬ G,Norm s\<turnstile>catch tn
lemma catch_XcptLoc:
G,(Some (XcptLoc a), s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C
lemma new_xcpt_var_def2:
new_xcpt_var vn (x, s) = Norm (lupd(Inl vn\<mapsto>Addr (the_XcptLoc (the x))) s)
lemma assign_Norm_Norm:
f v (Norm s) = Norm s' ==> assign f v (Norm s) = Norm s'
lemma assign_Norm_Some:
fst (f v (Norm s)) = Some y ==> assign f v (Norm s) = (Some y, s)
lemma assign_Some:
assign f v (Some x, s) = (Some x, s)
lemma assign_supd:
assign (%v. supd (f v)) v (x, s) = (x, if x = None then f v s else s)
lemma assign_raise_if:
assign (%v (x, s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) = ((raise_if (b s v) xcpt) x, if x = None & ¬ b s v then f v s else s)
lemma init_comp_ty_PrimT:
init_comp_ty (PrimT pt) = Skip
lemma target_IntVir:
target IntVir s a' t = obj_class (lookup_obj s a')
lemma target_notIntVir:
m ~= IntVir ==> target m s a' t = the_Class (RefT t)
lemma target_Static:
target Static s a' t = the_Class (RefT t)
lemma target_SuperM:
target SuperM s a' t = the_Class (RefT t)
lemma init_lvars_def2:
init_lvars G C sig mode a' pvs (x, s) =
(set_lvars
(init_vals (table_of (fst (snd (snd (the (cmethd G C sig))))))
(fst (snd (fst (snd (the (cmethd G C sig)))))[|->]pvs) (+)
(if mode = Static then empty else empty(()|->a'))))
(if mode = Static then x else (np a') x, s)
lemma body_def2:
body G C sig = split (%D. split (%x1. split (%x2. split (Body D)))) (the (cmethd G C sig))
lemma fvar_def2:
fvar C stat fn a' s =
((the (snd (the (globs (snd s) (if stat then Inr C else Inl (the_Addr a'))))
(Inl (fn, C))),
%v. supd (upd_gobj (if stat then Inr C else Inl (the_Addr a')) (Inl (fn, C))
v)),
xupd (if stat then id else np a') s)
lemma avar_def2:
avar G i' a' s =
((the (snd (snd (the_Arr (globs (snd s) (Inl (the_Addr a')))))
(Inr (the_Intg i'))),
%v (x, s').
((raise_if
(¬ G,s'\<turnstile>v fits fst (the_Arr
(globs (snd s) (Inl (the_Addr a')))))
ArrStore)
x,
upd_gobj (Inl (the_Addr a')) (Inr (the_Intg i')) v s')),
xupd (raise_if
(¬ the_Intg i'
in_bounds fst (snd (the_Arr (globs (snd s) (Inl (the_Addr a'))))))
IndOutBound o
np a')
s)
theorem eval_induct_:
[| G|-xd -xc>-> (xb, xa);
!!s t xc. P (Some xc, s) t (arbitrary3 t) (Some xc, s);
!!s. P (Norm s) (In1r Skip) dummy_res (Norm s);
!!s0. P (Norm s0) (In3 []) (In3 []) (Norm s0);
!!e es s0 s1 s2 v vs.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
G|-s1 -es#>vs-> s2; P s1 (In3 es) (In3 vs) s2 |]
==> P (Norm s0) (In3 (e # es)) (In3 (v # vs)) s2;
!!s vn. P (Norm s) (In2 (LVar vn)) (In2 (lvar vn s)) (Norm s);
!!T e s0 s1 s2 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
s2 = xupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1 |]
==> P (Norm s0) (In1l (Cast T e)) (In1 v) s2;
!!T b e s0 s1 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
b = (v ~= Null & G,snd s1\<turnstile>v fits RefT T) |]
==> P (Norm s0) (In1l (e InstOf T)) (In1 (Bool b)) s1;
!!s v. P (Norm s) (In1l (Lit v)) (In1 v) (Norm s);
!!s. P (Norm s) (In1l Super) (In1 (the (locals s (Inr ())))) (Norm s);
!!f s0 s1 v va.
[| G|-Norm s0 -va=>(v, f)-> s1; P (Norm s0) (In2 va) (In2 (v, f)) s1 |]
==> P (Norm s0) (In1l (Acc va)) (In1 v) s1;
!!e s0 s1 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1 |]
==> P (Norm s0) (In1r (Expr e)) dummy_res s1;
!!c1 c2 s0 s1 s2.
[| G|-Norm s0 -c1-> s1; P (Norm s0) (In1r c1) dummy_res s1;
G|-s1 -c2-> s2; P s1 (In1r c2) dummy_res s2 |]
==> P (Norm s0) (In1r (c1;; c2)) dummy_res s2;
!!C s0 s1 sig v.
[| G|-Norm s0 -body G C sig->v-> s1;
P (Norm s0) (In1l (body G C sig)) (In1 v) s1 |]
==> P (Norm s0) (In1l (Methd C sig)) (In1 v) s1;
!!D c e s0 s1 s2 s3 v.
[| G|-Norm s0 -init D-> s1; P (Norm s0) (In1r (init D)) dummy_res s1;
G|-s1 -c-> s2; P s1 (In1r c) dummy_res s2; G|-s2 -e->v-> s3;
P s2 (In1l e) (In1 v) s3 |]
==> P (Norm s0) (In1l (Body D c e)) (In1 v) s3;
!!b e0 e1 e2 s0 s1 s2 v.
[| G|-Norm s0 -e0->b-> s1; P (Norm s0) (In1l e0) (In1 b) s1;
G|-s1 -(if the_Bool b then e1 else e2)->v-> s2;
P s1 (In1l (if the_Bool b then e1 else e2)) (In1 v) s2 |]
==> P (Norm s0) (In1l (e0 ? e1 : e2)) (In1 v) s2;
!!b c1 c2 e s0 s1 s2.
[| G|-Norm s0 -e->b-> s1; P (Norm s0) (In1l e) (In1 b) s1;
G|-s1 -(if the_Bool b then c1 else c2)-> s2;
P s1 (In1r (if the_Bool b then c1 else c2)) dummy_res s2 |]
==> P (Norm s0) (In1r (If(e) c1 Else c2)) dummy_res s2;
!!b c e s0 s1 s2 s3.
[| G|-Norm s0 -e->b-> s1; P (Norm s0) (In1l e) (In1 b) s1;
if the_Bool b
then (G|-s1 -c-> s2 & P s1 (In1r c) dummy_res s2) &
G|-s2 -While(e) c-> s3 & P s2 (In1r (While(e) c)) dummy_res s3
else s3 = s1 |]
==> P (Norm s0) (In1r (While(e) c)) dummy_res s3;
!!c1 c2 s0 s1 s2 x1.
[| G|-Norm s0 -c1-> (x1, s1); P (Norm s0) (In1r c1) dummy_res (x1, s1);
G|-Norm s1 -c2-> s2; P (Norm s1) (In1r c2) dummy_res s2 |]
==> P (Norm s0) (In1r (c1 Finally c2)) dummy_res
(xupd (xcpt_if (x1 ~= None) x1) s2);
!!a' e s0 s1.
[| G|-Norm s0 -e->a'-> s1; P (Norm s0) (In1l e) (In1 a') s1 |]
==> P (Norm s0) (In1r (Throw e)) dummy_res (xupd (throw a') s1);
!!C a s0 s1 s2.
[| G|-Norm s0 -init C-> s1; P (Norm s0) (In1r (init C)) dummy_res s1;
G|-s1 -halloc CInst C>a-> s2 |]
==> P (Norm s0) (In1l (NewC C)) (In1 (Addr a)) s2;
!!T a e i' s0 s1 s2 s3.
[| G|-Norm s0 -init_comp_ty T-> s1;
P (Norm s0) (In1r (init_comp_ty T)) dummy_res s1; G|-s1 -e->i'-> s2;
P s1 (In1l e) (In1 i') s2;
G|-xupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3 |]
==> P (Norm s0) (In1l (New T[e])) (In1 (Addr a)) s3;
!!C fs ini ms s0 s1 s2 s3 sc si.
[| the (class G C) = (sc, si, fs, ms, ini);
if inited C (globs s0) then s3 = Norm s0
else (G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip else init sc)-> s1 &
P (Norm ((init_class_obj G C) s0))
(In1r (if C = Object then Skip else init sc)) dummy_res s1) &
(G|-(set_lvars empty) s1 -ini-> s2 &
P ((set_lvars empty) s1) (In1r ini) dummy_res s2) &
s3 = (set_lvars (locals (snd s1))) s2 |]
==> P (Norm s0) (In1r (init C)) dummy_res s3;
!!e f s0 s1 s2 v va w.
[| G|-Norm s0 -va=>(w, f)-> s1; P (Norm s0) (In2 va) (In2 (w, f)) s1;
G|-s1 -e->v-> s2; P s1 (In1l e) (In1 v) s2 |]
==> P (Norm s0) (In1l (va:=e)) (In1 v) (assign f v s2);
!!C c1 c2 s0 s1 s2 s3 vn.
[| G|-Norm s0 -c1-> s1; P (Norm s0) (In1r c1) dummy_res s1;
G|-s1 -sxalloc-> s2;
if G,s2\<turnstile>catch C
then G|-new_xcpt_var vn s2 -c2-> s3 &
P (new_xcpt_var vn s2) (In1r c2) dummy_res s3
else s3 = s2 |]
==> P (Norm s0) (In1r (Try c1 Catch(C vn) c2)) dummy_res s3;
!!C a e fn s0 s1 s2 s2' stat v.
[| G|-Norm s0 -init C-> s1; P (Norm s0) (In1r (init C)) dummy_res s1;
G|-s1 -e->a-> s2; P s1 (In1l e) (In1 a) s2;
(v, s2') = fvar C stat fn a s2 |]
==> P (Norm s0) (In2 ({C,stat}e..fn)) (In2 v) s2';
!!a e1 e2 i s0 s1 s2 s2' v.
[| G|-Norm s0 -e1->a-> s1; P (Norm s0) (In1l e1) (In1 a) s1;
G|-s1 -e2->i-> s2; P s1 (In1l e2) (In1 i) s2;
(v, s2') = avar G i a s2 |]
==> P (Norm s0) (In2 (e1.[e2])) (In2 v) s2';
!!C a' args cT e mn mode pTs s0 s1 s2 s3 t v vs.
[| G|-Norm s0 -e->a'-> s1; P (Norm s0) (In1l e) (In1 a') s1;
G|-s1 -args#>vs-> s2; P s1 (In3 args) (In3 vs) s2;
C = target mode (snd s2) a' cT;
G|-init_lvars G C (mn, pTs) mode a' vs s2 -Methd C (mn, pTs)->v-> s3;
P (init_lvars G C (mn, pTs) mode a' vs s2) (In1l (Methd C (mn, pTs)))
(In1 v) s3 |]
==> P (Norm s0) (In1l ({t,cT,mode}e..mn( {pTs}args))) (In1 v)
((set_lvars (locals (snd s2))) s3) |]
==> P xd xc xb xa
[!]
lemmas eval_induct:
[| G|-xd -xc>-> (xb, xa);
!!s t xc. P (Some xc, s) t (arbitrary3 t) (Some xc, s);
!!s. P (Norm s) (In1r Skip) dummy_res (Norm s);
!!s0. P (Norm s0) (In3 []) (In3 []) (Norm s0);
!!e es s0 s1 s2 v vs.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
G|-s1 -es#>vs-> s2; P s1 (In3 es) (In3 vs) s2 |]
==> P (Norm s0) (In3 (e # es)) (In3 (v # vs)) s2;
!!s vn. P (Norm s) (In2 (LVar vn)) (In2 (lvar vn s)) (Norm s);
!!T e s0 s1 s2 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
s2 = xupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1 |]
==> P (Norm s0) (In1l (Cast T e)) (In1 v) s2;
!!T b e s0 s1 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1;
b = (v ~= Null & G,snd s1\<turnstile>v fits RefT T) |]
==> P (Norm s0) (In1l (e InstOf T)) (In1 (Bool b)) s1;
!!s v. P (Norm s) (In1l (Lit v)) (In1 v) (Norm s);
!!s. P (Norm s) (In1l Super) (In1 (the (locals s (Inr ())))) (Norm s);
!!f s0 v va x y.
[| G|-Norm s0 -va=>(v, f)-> (x, y);
P (Norm s0) (In2 va) (In2 (v, f)) (x, y) |]
==> P (Norm s0) (In1l (Acc va)) (In1 v) (x, y);
!!e s0 s1 v.
[| G|-Norm s0 -e->v-> s1; P (Norm s0) (In1l e) (In1 v) s1 |]
==> P (Norm s0) (In1r (Expr e)) dummy_res s1;
!!c1 c2 s0 s1 x y.
[| G|-Norm s0 -c1-> s1; P (Norm s0) (In1r c1) dummy_res s1;
G|-s1 -c2-> (x, y); P s1 (In1r c2) dummy_res (x, y) |]
==> P (Norm s0) (In1r (c1;; c2)) dummy_res (x, y);
!!C s0 s1 sig v.
[| G|-Norm s0 -body G C sig->v-> s1;
P (Norm s0) (In1l (body G C sig)) (In1 v) s1 |]
==> P (Norm s0) (In1l (Methd C sig)) (In1 v) s1;
!!D c e s0 s1 s2 s3 v.
[| G|-Norm s0 -init D-> s1; P (Norm s0) (In1r (init D)) dummy_res s1;
G|-s1 -c-> s2; P s1 (In1r c) dummy_res s2; G|-s2 -e->v-> s3;
P s2 (In1l e) (In1 v) s3 |]
==> P (Norm s0) (In1l (Body D c e)) (In1 v) s3;
!!b e0 e1 e2 s0 s1 s2 v.
[| G|-Norm s0 -e0->b-> s1; P (Norm s0) (In1l e0) (In1 b) s1;
G|-s1 -(if the_Bool b then e1 else e2)->v-> s2;
P s1 (In1l (if the_Bool b then e1 else e2)) (In1 v) s2 |]
==> P (Norm s0) (In1l (e0 ? e1 : e2)) (In1 v) s2;
!!b c1 c2 e s0 s1 s2.
[| G|-Norm s0 -e->b-> s1; P (Norm s0) (In1l e) (In1 b) s1;
G|-s1 -(if the_Bool b then c1 else c2)-> s2;
P s1 (In1r (if the_Bool b then c1 else c2)) dummy_res s2 |]
==> P (Norm s0) (In1r (If(e) c1 Else c2)) dummy_res s2;
!!b c e s0 s1 s2 s3.
[| G|-Norm s0 -e->b-> s1; P (Norm s0) (In1l e) (In1 b) s1;
if the_Bool b
then (G|-s1 -c-> s2 & P s1 (In1r c) dummy_res s2) &
G|-s2 -While(e) c-> s3 & P s2 (In1r (While(e) c)) dummy_res s3
else s3 = s1 |]
==> P (Norm s0) (In1r (While(e) c)) dummy_res s3;
!!c1 c2 s0 s1 x1 x y.
[| G|-Norm s0 -c1-> (x1, s1); P (Norm s0) (In1r c1) dummy_res (x1, s1);
G|-Norm s1 -c2-> (x, y); P (Norm s1) (In1r c2) dummy_res (x, y) |]
==> P (Norm s0) (In1r (c1 Finally c2)) dummy_res
(xupd (xcpt_if (x1 ~= None) x1) (x, y));
!!a' e s0 s1.
[| G|-Norm s0 -e->a'-> s1; P (Norm s0) (In1l e) (In1 a') s1 |]
==> P (Norm s0) (In1r (Throw e)) dummy_res (xupd (throw a') s1);
!!C a s0 s1 x y.
[| G|-Norm s0 -init C-> s1; P (Norm s0) (In1r (init C)) dummy_res s1;
G|-s1 -halloc CInst C>a-> (x, y) |]
==> P (Norm s0) (In1l (NewC C)) (In1 (Addr a)) (x, y);
!!T a e i' s0 s1 s2 s3.
[| G|-Norm s0 -init_comp_ty T-> s1;
P (Norm s0) (In1r (init_comp_ty T)) dummy_res s1; G|-s1 -e->i'-> s2;
P s1 (In1l e) (In1 i') s2;
G|-xupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3 |]
==> P (Norm s0) (In1l (New T[e])) (In1 (Addr a)) s3;
!!C fs ini ms s0 s1 s2 s3 sc si.
[| the (class G C) = (sc, si, fs, ms, ini);
if inited C (globs s0) then s3 = Norm s0
else (G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip else init sc)-> s1 &
P (Norm ((init_class_obj G C) s0))
(In1r (if C = Object then Skip else init sc)) dummy_res s1) &
(G|-(set_lvars empty) s1 -ini-> s2 &
P ((set_lvars empty) s1) (In1r ini) dummy_res s2) &
s3 = (set_lvars (locals (snd s1))) s2 |]
==> P (Norm s0) (In1r (init C)) dummy_res s3;
!!e f s0 s1 s2 v va w.
[| G|-Norm s0 -va=>(w, f)-> s1; P (Norm s0) (In2 va) (In2 (w, f)) s1;
G|-s1 -e->v-> s2; P s1 (In1l e) (In1 v) s2 |]
==> P (Norm s0) (In1l (va:=e)) (In1 v) (assign f v s2);
!!C c1 c2 s0 s1 s2 s3 vn.
[| G|-Norm s0 -c1-> s1; P (Norm s0) (In1r c1) dummy_res s1;
G|-s1 -sxalloc-> s2;
if G,s2\<turnstile>catch C
then G|-new_xcpt_var vn s2 -c2-> s3 &
P (new_xcpt_var vn s2) (In1r c2) dummy_res s3
else s3 = s2 |]
==> P (Norm s0) (In1r (Try c1 Catch(C vn) c2)) dummy_res s3;
!!C a e fn s0 s1 s2 s2' stat v.
[| G|-Norm s0 -init C-> s1; P (Norm s0) (In1r (init C)) dummy_res s1;
G|-s1 -e->a-> s2; P s1 (In1l e) (In1 a) s2;
(v, s2') = fvar C stat fn a s2 |]
==> P (Norm s0) (In2 ({C,stat}e..fn)) (In2 v) s2';
!!a e1 e2 i s0 s1 s2 s2' v.
[| G|-Norm s0 -e1->a-> s1; P (Norm s0) (In1l e1) (In1 a) s1;
G|-s1 -e2->i-> s2; P s1 (In1l e2) (In1 i) s2;
(v, s2') = avar G i a s2 |]
==> P (Norm s0) (In2 (e1.[e2])) (In2 v) s2';
!!C a' args cT e mn mode pTs s0 s1 s2 s3 t v vs.
[| G|-Norm s0 -e->a'-> s1; P (Norm s0) (In1l e) (In1 a') s1;
G|-s1 -args#>vs-> s2; P s1 (In3 args) (In3 vs) s2;
C = target mode (snd s2) a' cT;
G|-init_lvars G C (mn, pTs) mode a' vs s2 -Methd C (mn, pTs)->v-> s3;
P (init_lvars G C (mn, pTs) mode a' vs s2) (In1l (Methd C (mn, pTs)))
(In1 v) s3 |]
==> P (Norm s0) (In1l ({t,cT,mode}e..mn( {pTs}args))) (In1 v)
((set_lvars (locals (snd s2))) s3) |]
==> P xd xc xb xa
[!]
lemma sxalloc_elim_cases2:
[| G|-s -sxalloc-> s'; !!s. s' = Norm s ==> P;
!!a s. s' = (Some (XcptLoc a), s) ==> P |]
==> P
[!]
lemma eval_Inj_elim:
G|-s -t>-> (w, s')
==> sum3_case ((%e. EX v. w = In1 v) (+) (%c. w = dummy_res))
(%e. EX v. w = In2 v) (%e. EX v. w = In3 v) t
[!]
theorem eval_expr_eq:
G|-s -In1l t>-> (w, s') = (EX v. w = In1 v & G|-s -t->v-> s') [!]
theorem eval_var_eq:
G|-s -In2 t>-> (w, s') = (EX vf. w = In2 vf & G|-s -t=>vf-> s') [!]
theorem eval_exprs_eq:
G|-s -In3 t>-> (w, s') = (EX vs. w = In3 vs & G|-s -t#>vs-> s') [!]
theorem eval_stmt_eq:
G|-s -In1r t>-> (w, s') = (w = dummy_res & G|-s -t-> s') [!]
theorems XcptIs:
G|-(Some xc, s) -x->arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x=>arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x#>arbitrary-> (Some xc, s) [!]
G|-(Some xc, s) -x-> (Some xc, s) [!]
lemma eval_no_xcpt_lemma:
G|-s -t>-> (w, s') ==> normal s' --> normal s [!]
lemma eval_no_xcpt:
G|-(x, s) -t>-> (w, Norm s') = (x = None & G|-Norm s -t>-> (w, Norm s')) [!]
lemma eval_xcpt_lemma:
G|-s -t>-> (v, s') ==> fst s = Some xc --> s' = s & v = arbitrary3 t [!]
lemma eval_xcpt:
G|-(Some xc, s) -t>-> (w, s') =
(s' = (Some xc, s) &
w = arbitrary3 t & G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s))
[!]
lemma LitI:
G|-s -Lit v->(if normal s then v else arbitrary)-> s [!]
lemma SkipI:
G|-s -Skip-> s [!]
lemma ExprI:
G|-s -e->v-> s' ==> G|-s -Expr e-> s' [!]
lemma CompI:
[| G|-s -c1-> s1; G|-s1 -c2-> s2 |] ==> G|-s -c1;; c2-> s2 [!]
lemma CondI:
[| G|-s -e->b-> s1; G|-s1 -(if the_Bool b then e1 else e2)->v-> s2 |]
==> G|-s -e ? e1 : e2->(if normal s1 then v else arbitrary)-> s2
[!]
lemma IfI:
[| G|-s -e->v-> s1; G|-s1 -(if the_Bool v then c1 else c2)-> s2 |]
==> G|-s -If(e) c1 Else c2-> s2
[!]
lemma MethdI:
G|-s -body G C sig->v-> s' ==> G|-s -Methd C sig->v-> s' [!]
lemma eval_Call:
[| G|-Norm s0 -e->a'-> s1; G|-s1 -ps#>pvs-> s2; C = target mode (snd s2) a' cT;
G|-init_lvars G C (mn, pTs) mode a' pvs s2 -Methd C (mn, pTs)->v-> s3;
s3' = (set_lvars (locals (snd s2))) s3 |]
==> G|-Norm s0 -{t,cT,mode}e..mn( {pTs}ps)->v-> s3'
[!]
lemma eval_Init:
if inited C (globs s0) then s3 = Norm s0
else G|-Norm ((init_class_obj G C)
s0) -(if C = Object then Skip
else init (fst (the (class G C))))-> s1 &
G|-(set_lvars empty) s1 -snd (snd (snd (snd (the (class G C)))))-> s2 &
s3 = (set_lvars (locals (snd s1))) s2
==> G|-Norm s0 -init C-> s3
[!]
lemma init_done:
initd C s ==> G|-s -init C-> s [!]
lemma eval_StatRef:
G|-s -StatRef rt->(if fst s = None then Null else arbitrary)-> s [!]
lemma SkipD:
G|-s -Skip-> s' ==> s' = s [!]
lemma Skip_eq:
G|-s -Skip-> s' = (s = s') [!]
lemma init_retains_locals:
[| G|-s -t>-> (w, s'); t = In1r (init C) |] ==> locals (snd s) = locals (snd s')
[!]
lemma halloc_xcpt:
G|-(Some xc, s) -halloc oi>a-> s' ==> s' = (Some xc, s) [!]
lemma eval_Methd:
G|-s -In1l (body G C sig)>-> (w, s') ==> G|-s -In1l (Methd C sig)>-> (w, s')
[!]
lemma unique_halloc:
[| (s, oi, as) : halloc G; (s, oi, as') : halloc G |] ==> as' = as [!]
lemma single_valued_halloc:
single_valued {((s, oi), a, s'). G|-s -halloc oi>a-> s'} [!]
lemma unique_sxalloc:
[| G|-s -sxalloc-> s'; G|-s -sxalloc-> s'' |] ==> s'' = s' [!]
lemma single_valued_sxalloc:
single_valued {(s, s'). G|-s -sxalloc-> s'} [!]
lemma split_pairD:
(x, y) = p ==> x = fst p & y = snd p
lemma unique_eval:
[| G|-s -t>-> ws; G|-s -t>-> ws' |] ==> ws' = ws [!]
lemma single_valued_eval:
single_valued {((s, t), vs'). G|-s -t>-> vs'} [!]