src/HOL/Bali/Trans.thy
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13354 8c8eafb63746
     1.1 --- a/src/HOL/Bali/Trans.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -7,175 +7,434 @@
     1.4  execution of Java expressions and statements
     1.5  
     1.6  PRELIMINARY!!!!!!!!
     1.7 -
     1.8 -improvements over Java Specification 1.0 (cf. 15.11.4.4):
     1.9 -* dynamic method lookup does not need to check the return type
    1.10 -* throw raises a NullPointer exception if a null reference is given, and each
    1.11 -  throw of a system exception yield a fresh exception object (was not specified)
    1.12 -* if there is not enough memory even to allocate an OutOfMemory exception,
    1.13 -  evaluation/execution fails, i.e. simply stops (was not specified)
    1.14 -
    1.15 -design issues:
    1.16 -* Lit expressions and Skip statements are considered completely evaluated.
    1.17 -* the expr entry in rules is redundant in case of exceptions, but its full
    1.18 -  inclusion helps to make the rule structure independent of exception occurence.
    1.19 -* the rule format is such that the start state may contain an exception.
    1.20 -  ++ faciliates exception handling (to be added later)
    1.21 -  +  symmetry
    1.22 -* the rules are defined carefully in order to be applicable even in not
    1.23 -  type-correct situations (yielding undefined values),
    1.24 -  e.g. the_Adr (Val (Bool b)) = arbitrary.
    1.25 -  ++ fewer rules 
    1.26 -  -  less readable because of auxiliary functions like the_Adr
    1.27 -  Alternative: "defensive" evaluation throwing some InternalError exception
    1.28 -               in case of (impossible, for correct programs) type mismatches
    1.29 -
    1.30 -simplifications:
    1.31 -* just simple handling (i.e. propagation) of exceptions so far
    1.32 -* dynamic method lookup does not check return type (should not be necessary)
    1.33  *)
    1.34  
    1.35 -Trans = Eval +
    1.36 +theory Trans = Evaln:
    1.37 +(*
    1.38 +constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
    1.39 +    "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
    1.40 +
    1.41 +constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
    1.42 +    "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
    1.43 +*)
    1.44 +axclass inj_term < "type"
    1.45 +consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
    1.46 +
    1.47 +instance stmt::inj_term ..
    1.48 +
    1.49 +defs (overloaded)
    1.50 +stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.51 +
    1.52 +lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    1.53 +by (simp add: stmt_inj_term_def)
    1.54 +
    1.55 +instance expr::inj_term ..
    1.56 +
    1.57 +defs (overloaded)
    1.58 +expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.59 +
    1.60 +lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    1.61 +by (simp add: expr_inj_term_def)
    1.62 +
    1.63 +instance var::inj_term ..
    1.64 +
    1.65 +defs (overloaded)
    1.66 +var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.67 +
    1.68 +lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
    1.69 +by (simp add: var_inj_term_def)
    1.70 +
    1.71 +instance "list":: (type) inj_term ..
    1.72 +
    1.73 +defs (overloaded)
    1.74 +expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
    1.75 +
    1.76 +lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
    1.77 +by (simp add: expr_list_inj_term_def)
    1.78 +
    1.79 +constdefs groundVar:: "var \<Rightarrow> bool"
    1.80 +"groundVar v \<equiv> (case v of
    1.81 +                   LVar ln \<Rightarrow> True
    1.82 +                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
    1.83 +                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
    1.84 +                 | InsInitV c v \<Rightarrow> False)"
    1.85 +
    1.86 +lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
    1.87 +  assumes ground: "groundVar v" and
    1.88 +          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
    1.89 +          FVar: "\<And> accC statDeclC stat a fn. 
    1.90 +                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
    1.91 +          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
    1.92 +  shows "P"
    1.93 +proof -
    1.94 +  from ground LVar FVar AVar
    1.95 +  show ?thesis
    1.96 +    apply (cases v)
    1.97 +    apply (simp add: groundVar_def)
    1.98 +    apply (simp add: groundVar_def,blast)
    1.99 +    apply (simp add: groundVar_def,blast)
   1.100 +    apply (simp add: groundVar_def)
   1.101 +    done
   1.102 +qed
   1.103 +
   1.104 +constdefs groundExprs:: "expr list \<Rightarrow> bool"
   1.105 +"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
   1.106 +  
   1.107 +consts the_val:: "expr \<Rightarrow> val"
   1.108 +primrec
   1.109 +"the_val (Lit v) = v"
   1.110 +
   1.111 +consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
   1.112 +primrec
   1.113 +"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
   1.114 +the_var_FVar_def:
   1.115 +"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
   1.116 +the_var_AVar_def:
   1.117 +"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
   1.118 +
   1.119 +lemma the_var_FVar_simp[simp]:
   1.120 +"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
   1.121 +by (simp)
   1.122 +declare the_var_FVar_def [simp del]
   1.123 +
   1.124 +lemma the_var_AVar_simp:
   1.125 +"the_var G s ((Lit a).[Lit i]) = avar G i a s"
   1.126 +by (simp)
   1.127 +declare the_var_AVar_def [simp del]
   1.128  
   1.129  consts
   1.130 -  texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
   1.131 -		            ((stmt  state)  (stmt  state))) set"
   1.132 +  step	:: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
   1.133  
   1.134  syntax (symbols)
   1.135 -  texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
   1.136 -  tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
   1.137 -  Ref   :: "loc  expr"
   1.138 +  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
   1.139 +  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" 
   1.140 +                                                  ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
   1.141 +"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
   1.142 +  Ref  :: "loc \<Rightarrow> expr"
   1.143 +  SKIP :: "expr"
   1.144  
   1.145  translations
   1.146 -
   1.147 -  "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
   1.148 -  "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
   1.149 +  "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
   1.150 +  "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
   1.151 +  "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
   1.152    "Ref a" == "Lit (Addr a)"
   1.153 +  "SKIP"  == "Lit Unit"
   1.154  
   1.155 -constdefs
   1.156 -  
   1.157 -  sub_expr_expr :: "(expr  expr)  prop"
   1.158 -  "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
   1.159 -				     G(ef e,s) 1 (ef e',s'))"
   1.160 -
   1.161 -inductive "texpr_tstmt G" intrs 
   1.162 +inductive "step G" intros 
   1.163  
   1.164  (* evaluation of expression *)
   1.165    (* cf. 15.5 *)
   1.166 -  XcptE	"v. e  Lit v 
   1.167 -				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
   1.168 -
   1.169 - CastXX "PROP sub_expr_expr (Cast T)"
   1.170 -
   1.171 -(*
   1.172 -  (* cf. 15.8.1 *)
   1.173 -  NewC	"new_Addr (heap s) = Some (a,x);
   1.174 -	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
   1.175 -				G(NewC C,None,s) 1 (Ref a,s')"
   1.176 -
   1.177 -  (* cf. 15.9.1 *)
   1.178 -(*NewA1	"sub_expr_expr (NewA T)"*)
   1.179 -  NewA1	"G(e,None,s) 1 (e',s') 
   1.180 -			      G(New T[e],None,s) 1 (New T[e'],s')"
   1.181 -  NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
   1.182 -	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
   1.183 -			G(New T[Lit i'],None,s) 1 (Ref a,s')"
   1.184 -  (* cf. 15.15 *)
   1.185 -  Cast1	"G(e,None,s) 1 (e',s') 
   1.186 -			      G(Cast T e,None,s) 1 (Cast T e',s')"
   1.187 -  Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
   1.188 -		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
   1.189 +Abrupt:	         "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
   1.190 +                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
   1.191 +                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
   1.192 +                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
   1.193 +                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
   1.194 +                \<Longrightarrow> 
   1.195 +                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
   1.196  
   1.197 -  (* cf. 15.7.1 *)
   1.198 -(*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
   1.199 -
   1.200 -  (* cf. 15.13.1, 15.2 *)
   1.201 -  LAcc	"v = the (locals s vn) 
   1.202 -			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
   1.203 -
   1.204 -  (* cf. 15.25.1 *)
   1.205 -  LAss1	"G(e,None,s) 1 (e',s') 
   1.206 -				 G(f vn:=e,None,s) 1 (vn:=e',s')"
   1.207 -  LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
   1.208 +InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
   1.209 +           \<Longrightarrow> 
   1.210 +           G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
   1.211  
   1.212 -  (* cf. 15.10.1, 15.2 *)
   1.213 -  FAcc1	"G(e,None,s) 1 (e',s') 
   1.214 -			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
   1.215 -  FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
   1.216 -			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
   1.217 -
   1.218 -  (* cf. 15.25.1 *)
   1.219 -  FAss1	"G(e1,None,s) 1 (e1',s') 
   1.220 -			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
   1.221 -  FAss2	"G(e2,np a' None,s) 1 (e2',s') 
   1.222 -		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
   1.223 -  FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
   1.224 -	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
   1.225 -		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
   1.226 -
   1.227 -
   1.228 +(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
   1.229 +(* Specialised rules to evaluate: 
   1.230 +   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
   1.231 + 
   1.232 +  (* cf. 15.8.1 *)
   1.233 +NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
   1.234 +NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
   1.235 +             \<Longrightarrow> 
   1.236 +             G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
   1.237  
   1.238  
   1.239  
   1.240 -  (* cf. 15.12.1 *)
   1.241 -  AAcc1	"G(e1,None,s) 1 (e1',s') 
   1.242 -				G(e1[e2],None,s) 1 (e1'[e2],s')"
   1.243 -  AAcc2	"G(e2,None,s) 1 (e2',s') 
   1.244 -			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
   1.245 -  AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
   1.246 -	  x' = raise_if (vo = None) IndOutBound (np a' None) 
   1.247 -			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
   1.248 +(* Alternative when rule SeqE is present 
   1.249 +NewCInited: "\<lbrakk>inited C (globs s); 
   1.250 +              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
   1.251 +             \<Longrightarrow> 
   1.252 +              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
   1.253 +
   1.254 +NewC:
   1.255 +     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
   1.256 +     \<Longrightarrow> 
   1.257 +      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
   1.258 +
   1.259 +*)
   1.260 +  (* cf. 15.9.1 *)
   1.261 +NewA: 
   1.262 +   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
   1.263 +InsInitNewAIdx: 
   1.264 +   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
   1.265 +    \<Longrightarrow>  
   1.266 +    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
   1.267 +InsInitNewA: 
   1.268 +   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
   1.269 +    \<Longrightarrow>
   1.270 +    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
   1.271 + 
   1.272 +  (* cf. 15.15 *)
   1.273 +CastE:	
   1.274 +   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.275 +    \<Longrightarrow>
   1.276 +    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
   1.277 +Cast:	
   1.278 +   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
   1.279 +    \<Longrightarrow> 
   1.280 +    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.281 +  (* can be written without abupd, since we know Norm s *)
   1.282  
   1.283  
   1.284 -  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
   1.285 -  Call1	"G(e,None,s) 1 (e',s') 
   1.286 -			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
   1.287 -  Call2	"G(p,None,s) 1 (p',s') 
   1.288 -		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
   1.289 -  Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
   1.290 - 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
   1.291 -	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
   1.292 -      (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
   1.293 -  Body1	"G(s0,None,s) 1 (s0',s') 
   1.294 -		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
   1.295 -  Body2	"G(e ,None,s) 1 (e',s') 
   1.296 -		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
   1.297 -  Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
   1.298 +InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
   1.299 +        \<Longrightarrow> 
   1.300 +        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
   1.301 +Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
   1.302 +        \<Longrightarrow> 
   1.303 +        G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
   1.304 +
   1.305 +  (* cf. 15.7.1 *)
   1.306 +(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
   1.307 +
   1.308 +UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
   1.309 +         \<Longrightarrow> 
   1.310 +         G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
   1.311 +UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
   1.312 +
   1.313 +BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
   1.314 +           \<Longrightarrow> 
   1.315 +           G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
   1.316 +BinOpE2:  "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
   1.317 +           \<Longrightarrow> 
   1.318 +           G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
   1.319 +            \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
   1.320 +BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
   1.321 +            \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
   1.322 +
   1.323 +Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
   1.324 +
   1.325 +AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
   1.326 +        \<Longrightarrow> 
   1.327 +        G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
   1.328 +Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
   1.329 +       \<Longrightarrow>  
   1.330 +       G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.331 +
   1.332 +(*
   1.333 +AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
   1.334 +AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
   1.335 +          \<Longrightarrow>  
   1.336 +          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
   1.337 +           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.338 +AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
   1.339 +          \<Longrightarrow>  
   1.340 +          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.341 +*) 
   1.342 +AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
   1.343 +         \<Longrightarrow> 
   1.344 +         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
   1.345 +AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.346 +         \<Longrightarrow> 
   1.347 +         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
   1.348 +Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
   1.349 +         \<Longrightarrow> 
   1.350 +         G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
   1.351 +
   1.352 +CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
   1.353 +        \<Longrightarrow> 
   1.354 +        G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
   1.355 +Cond:  "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)"
   1.356 +
   1.357 +
   1.358 +CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.359 +             \<Longrightarrow>
   1.360 +	     G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.361 +              \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
   1.362 +CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
   1.363 +             \<Longrightarrow>
   1.364 +	     G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.365 +              \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
   1.366 +Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
   1.367 +              D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.368 +              s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
   1.369 +             \<Longrightarrow> 
   1.370 +             G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.371 +              \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
   1.372 +           
   1.373 +Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
   1.374 +             \<Longrightarrow> 
   1.375 +             G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
   1.376 +
   1.377 +CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
   1.378 +               \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
   1.379 +
   1.380 +Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
   1.381 +
   1.382 +Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
   1.383 +
   1.384 +InsInitBody: 
   1.385 +    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
   1.386 +     \<Longrightarrow> 
   1.387 +     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
   1.388 +InsInitBodyRet: 
   1.389 +     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
   1.390 +       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
   1.391 +
   1.392 +(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
   1.393 +  
   1.394 +FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
   1.395 +       \<Longrightarrow> 
   1.396 +       G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
   1.397 +        \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
   1.398 +InsInitFVarE:
   1.399 +      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
   1.400 +       \<Longrightarrow>
   1.401 +       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
   1.402 +        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
   1.403 +InsInitFVar:
   1.404 +      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
   1.405 +        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
   1.406 +--  {* Notice, that we do not have literal values for @{text vars}. 
   1.407 +The rules for accessing variables (@{text Acc}) and assigning to variables 
   1.408 +(@{text Ass}), test this with the predicate @{text groundVar}.  After 
   1.409 +initialisation is done and the @{text FVar} is evaluated, we can't just 
   1.410 +throw away the @{text InsInitFVar} term and return a literal value, as in the 
   1.411 +cases of @{text New}  or @{text NewC}. Instead we just return the evaluated 
   1.412 +@{text FVar} and test for initialisation in the rule @{text FVar}. 
   1.413 +*}
   1.414 +
   1.415 +
   1.416 +AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
   1.417 +         \<Longrightarrow> 
   1.418 +         G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
   1.419 +
   1.420 +AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
   1.421 +         \<Longrightarrow> 
   1.422 +         G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
   1.423 +
   1.424 +(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
   1.425 +
   1.426 +(* evaluation of expression lists *)
   1.427 +
   1.428 +  -- {* @{text Nil}  is fully evaluated *}
   1.429 +
   1.430 +ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
   1.431 +         \<Longrightarrow>
   1.432 +         G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
   1.433 +  
   1.434 +ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
   1.435 +         \<Longrightarrow>
   1.436 +         G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
   1.437  
   1.438  (* execution of statements *)
   1.439  
   1.440 -  (* cf. 14.1 *)
   1.441 -  XcptS	"s0  Skip 
   1.442 -				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
   1.443 -
   1.444    (* cf. 14.5 *)
   1.445 -(*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
   1.446 +Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.447  
   1.448 -  (* cf. 14.2 *)
   1.449 -  Comp1	"G(s1,None,s) 1 (s1',s') 
   1.450 -			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
   1.451 -  Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
   1.452 -
   1.453 -
   1.454 -
   1.455 -
   1.456 +ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.457 +        \<Longrightarrow> 
   1.458 +        G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
   1.459 +Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.460  
   1.461  
   1.462 -  (* cf. 14.7 *)
   1.463 -  Expr1	"G(e ,None,s) 1 (e',s') 
   1.464 -				G(Expr e,None,s) 1 (Expr e',s')"
   1.465 -  Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
   1.466 +LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
   1.467 +       \<Longrightarrow>  
   1.468 +       G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
   1.469 +Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
   1.470 +
   1.471 +  (* cf. 14.2 *)
   1.472 +CompC1:	"\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.473 +         \<Longrightarrow> 
   1.474 +         G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
   1.475 +
   1.476 +Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
   1.477  
   1.478    (* cf. 14.8.2 *)
   1.479 -  If1	"G(e ,None,s) 1 (e',s') 
   1.480 -		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
   1.481 -  If		 "G(If(Lit v) s1 Else s2,None,s) 1 
   1.482 -		    (if the_Bool v then s1 else s2,None,s)"
   1.483 +IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.484 +      \<Longrightarrow>
   1.485 +      G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
   1.486 +If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
   1.487 +       \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
   1.488  
   1.489    (* cf. 14.10, 14.10.1 *)
   1.490 -  Loop			  "G(While(e) s0,None,s) 1 
   1.491 -			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
   1.492 +Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
   1.493 +        \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
   1.494 +
   1.495 +Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
   1.496 +
   1.497 +ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.498 +         \<Longrightarrow>
   1.499 +         G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
   1.500 +Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
   1.501 +
   1.502 +TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.503 +        \<Longrightarrow>
   1.504 +        G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
   1.505 +Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
   1.506 +        \<Longrightarrow>
   1.507 +        G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
   1.508 +         \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
   1.509 +                              else (\<langle>Skip\<rangle>,s'))"
   1.510 +
   1.511 +FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.512 +        \<Longrightarrow>
   1.513 +        G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
   1.514 +
   1.515 +Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
   1.516 +
   1.517 +FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
   1.518 +        \<Longrightarrow>
   1.519 +        G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
   1.520 +FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
   1.521 +
   1.522 +
   1.523 +Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
   1.524 +        \<Longrightarrow> 
   1.525 +        G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.526 +Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
   1.527 +       \<Longrightarrow> 
   1.528 +       G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
   1.529 +        \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
   1.530 +              Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
   1.531 +             ,Norm (init_class_obj G C s))"
   1.532 +-- {* @{text InsInitE} is just used as trick to embed the statement 
   1.533 +@{text "init c"} into an expression*} 
   1.534 +InsInitESKIP:
   1.535 +  "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.536 +         
   1.537 +(* Equivalenzen:
   1.538 +  Bigstep zu Smallstep komplett.
   1.539 +  Smallstep zu Bigstep, nur wenn nicht die Ausdrcke Callee, FinA ,\<dots>
   1.540  *)
   1.541 -  con_defs "[sub_expr_expr_def]"
   1.542  
   1.543 -end
   1.544 +lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
   1.545 +proof -
   1.546 +  assume "p \<in> R\<^sup>*"
   1.547 +  moreover obtain x y where p: "p = (x,y)" by (cases p)
   1.548 +  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
   1.549 +  hence "\<exists>n. (x,y) \<in> R^n"
   1.550 +  proof induct
   1.551 +    fix a have "(a,a) \<in> R^0" by simp
   1.552 +    thus "\<exists>n. (a,a) \<in> R ^ n" ..
   1.553 +  next
   1.554 +    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
   1.555 +    then obtain n where "(a,b) \<in> R^n" ..
   1.556 +    moreover assume "(b,c) \<in> R"
   1.557 +    ultimately have "(a,c) \<in> R^(Suc n)" by auto
   1.558 +    thus "\<exists>n. (a,c) \<in> R^n" ..
   1.559 +  qed
   1.560 +  with p show ?thesis by hypsubst
   1.561 +qed  
   1.562 +
   1.563 +(*
   1.564 +lemma imp_eval_trans:
   1.565 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
   1.566 +    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
   1.567 +*)
   1.568 +(* Jetzt muss man bei trans natrlich wieder unterscheiden: Stmt, Expr, Var!
   1.569 +   Sowas bldes:
   1.570 +   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
   1.571 +   the_vals definieren\<dots>
   1.572 +  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
   1.573 +*)
   1.574 +
   1.575 +
   1.576 +end
   1.577 \ No newline at end of file