src/HOL/Bali/Trans.thy
changeset 21765 89275a3ed7be
parent 16417 9bc16273c2d4
child 23747 b07cff284683
     1.1 --- a/src/HOL/Bali/Trans.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -60,29 +60,22 @@
     1.4  by (simp)
     1.5  declare the_var_AVar_def [simp del]
     1.6  
     1.7 -consts
     1.8 -  step	:: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
     1.9 -
    1.10 -syntax (symbols)
    1.11 -  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    1.12 -  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" 
    1.13 -                                                  ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
    1.14 -"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
    1.15 +syntax (xsymbols)
    1.16    Ref  :: "loc \<Rightarrow> expr"
    1.17    SKIP :: "expr"
    1.18  
    1.19  translations
    1.20 -  "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
    1.21 -  "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
    1.22 -  "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
    1.23    "Ref a" == "Lit (Addr a)"
    1.24    "SKIP"  == "Lit Unit"
    1.25  
    1.26 -inductive "step G" intros 
    1.27 +inductive2
    1.28 +  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    1.29 +  for G :: prog
    1.30 +where
    1.31  
    1.32  (* evaluation of expression *)
    1.33    (* cf. 15.5 *)
    1.34 -Abrupt:	         "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
    1.35 +  Abrupt:       "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
    1.36                    \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
    1.37                    \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
    1.38                    \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
    1.39 @@ -90,19 +83,19 @@
    1.40                  \<Longrightarrow> 
    1.41                    G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
    1.42  
    1.43 -InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
    1.44 -           \<Longrightarrow> 
    1.45 -           G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
    1.46 +| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
    1.47 +             \<Longrightarrow> 
    1.48 +             G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
    1.49  
    1.50  (* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
    1.51  (* Specialised rules to evaluate: 
    1.52     InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
    1.53   
    1.54    (* cf. 15.8.1 *)
    1.55 -NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
    1.56 -NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
    1.57 -             \<Longrightarrow> 
    1.58 -             G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
    1.59 +| NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
    1.60 +| NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
    1.61 +               \<Longrightarrow> 
    1.62 +               G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
    1.63  
    1.64  
    1.65  
    1.66 @@ -119,68 +112,68 @@
    1.67  
    1.68  *)
    1.69    (* cf. 15.9.1 *)
    1.70 -NewA: 
    1.71 +| NewA: 
    1.72     "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
    1.73 -InsInitNewAIdx: 
    1.74 +| InsInitNewAIdx: 
    1.75     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
    1.76      \<Longrightarrow>  
    1.77      G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
    1.78 -InsInitNewA: 
    1.79 +| InsInitNewA: 
    1.80     "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
    1.81      \<Longrightarrow>
    1.82      G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
    1.83   
    1.84    (* cf. 15.15 *)
    1.85 -CastE:	
    1.86 +| CastE:	
    1.87     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
    1.88      \<Longrightarrow>
    1.89      G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
    1.90 -Cast:	
    1.91 +| Cast:	
    1.92     "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
    1.93      \<Longrightarrow> 
    1.94      G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
    1.95    (* can be written without abupd, since we know Norm s *)
    1.96  
    1.97  
    1.98 -InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
    1.99 +| InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
   1.100          \<Longrightarrow> 
   1.101          G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
   1.102 -Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
   1.103 -        \<Longrightarrow> 
   1.104 -        G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
   1.105 +| Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
   1.106 +          \<Longrightarrow> 
   1.107 +          G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
   1.108  
   1.109    (* cf. 15.7.1 *)
   1.110  (*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
   1.111  
   1.112 -UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
   1.113 -         \<Longrightarrow> 
   1.114 -         G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
   1.115 -UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
   1.116 -
   1.117 -BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
   1.118 +| UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
   1.119             \<Longrightarrow> 
   1.120 -           G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
   1.121 -BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
   1.122 -           \<Longrightarrow> 
   1.123 -           G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
   1.124 -            \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
   1.125 -BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
   1.126 +           G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
   1.127 +| UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
   1.128 +
   1.129 +| BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
   1.130 +             \<Longrightarrow> 
   1.131 +             G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
   1.132 +| BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
   1.133               \<Longrightarrow> 
   1.134               G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
   1.135 -              \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
   1.136 -BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
   1.137 -            \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
   1.138 +              \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
   1.139 +| BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
   1.140 +               \<Longrightarrow> 
   1.141 +               G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
   1.142 +                \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
   1.143 +| BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
   1.144 +              \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
   1.145  (* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
   1.146     to make the choice between BinOpTerm and BinOp deterministic *)
   1.147     
   1.148 -Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
   1.149 +| Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
   1.150  
   1.151 -AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
   1.152 -        \<Longrightarrow> 
   1.153 -        G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
   1.154 -Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
   1.155 -       \<Longrightarrow>  
   1.156 -       G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.157 +| AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
   1.158 +          \<Longrightarrow> 
   1.159 +          G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
   1.160 +| Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
   1.161 +         \<Longrightarrow>  
   1.162 +         G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.163  
   1.164  (*
   1.165  AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
   1.166 @@ -192,68 +185,68 @@
   1.167            \<Longrightarrow>  
   1.168            G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
   1.169  *) 
   1.170 -AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
   1.171 -         \<Longrightarrow> 
   1.172 -         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
   1.173 -AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.174 -         \<Longrightarrow> 
   1.175 -         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
   1.176 -Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
   1.177 -         \<Longrightarrow> 
   1.178 -         G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
   1.179 +| AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
   1.180 +           \<Longrightarrow> 
   1.181 +           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
   1.182 +| AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.183 +           \<Longrightarrow> 
   1.184 +           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
   1.185 +| Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
   1.186 +           \<Longrightarrow> 
   1.187 +           G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
   1.188  
   1.189 -CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
   1.190 -        \<Longrightarrow> 
   1.191 -        G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
   1.192 -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.193 +| CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
   1.194 +          \<Longrightarrow> 
   1.195 +          G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
   1.196 +| 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.197  
   1.198  
   1.199 -CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.200 -             \<Longrightarrow>
   1.201 -	     G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.202 -              \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
   1.203 -CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
   1.204 -             \<Longrightarrow>
   1.205 -	     G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.206 -              \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
   1.207 -Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
   1.208 -              D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.209 -              s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
   1.210 -             \<Longrightarrow> 
   1.211 -             G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.212 -              \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
   1.213 +| CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.214 +               \<Longrightarrow>
   1.215 +               G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.216 +                \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
   1.217 +| CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
   1.218 +               \<Longrightarrow>
   1.219 +               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.220 +                \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
   1.221 +| Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
   1.222 +                D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.223 +                s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
   1.224 +               \<Longrightarrow> 
   1.225 +               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
   1.226 +                \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
   1.227             
   1.228 -Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
   1.229 -             \<Longrightarrow> 
   1.230 -             G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
   1.231 +| Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
   1.232 +               \<Longrightarrow> 
   1.233 +               G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
   1.234  
   1.235 -CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
   1.236 -               \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
   1.237 +| CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
   1.238 +                 \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
   1.239  
   1.240 -Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
   1.241 +| Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
   1.242  
   1.243 -Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
   1.244 +| Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
   1.245  
   1.246 -InsInitBody: 
   1.247 +| InsInitBody: 
   1.248      "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
   1.249       \<Longrightarrow> 
   1.250       G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
   1.251 -InsInitBodyRet: 
   1.252 +| InsInitBodyRet: 
   1.253       "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
   1.254         \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
   1.255  
   1.256  (*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
   1.257    
   1.258 -FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
   1.259 -       \<Longrightarrow> 
   1.260 -       G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
   1.261 -        \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
   1.262 -InsInitFVarE:
   1.263 +| FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
   1.264 +         \<Longrightarrow> 
   1.265 +         G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
   1.266 +          \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
   1.267 +| InsInitFVarE:
   1.268        "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
   1.269         \<Longrightarrow>
   1.270         G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
   1.271          \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
   1.272 -InsInitFVar:
   1.273 +| InsInitFVar:
   1.274        "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
   1.275          \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
   1.276  --  {* Notice, that we do not have literal values for @{text vars}. 
   1.277 @@ -266,13 +259,13 @@
   1.278  *}
   1.279  
   1.280  
   1.281 -AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
   1.282 -         \<Longrightarrow> 
   1.283 -         G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
   1.284 +| AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
   1.285 +           \<Longrightarrow> 
   1.286 +           G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
   1.287  
   1.288 -AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
   1.289 -         \<Longrightarrow> 
   1.290 -         G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
   1.291 +| AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
   1.292 +           \<Longrightarrow> 
   1.293 +           G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
   1.294  
   1.295  (* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
   1.296  
   1.297 @@ -280,89 +273,97 @@
   1.298  
   1.299    -- {* @{text Nil}  is fully evaluated *}
   1.300  
   1.301 -ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
   1.302 -         \<Longrightarrow>
   1.303 -         G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
   1.304 +| ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
   1.305 +           \<Longrightarrow>
   1.306 +           G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
   1.307    
   1.308 -ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
   1.309 -         \<Longrightarrow>
   1.310 -         G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
   1.311 +| ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
   1.312 +           \<Longrightarrow>
   1.313 +           G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
   1.314  
   1.315  (* execution of statements *)
   1.316  
   1.317    (* cf. 14.5 *)
   1.318 -Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.319 +| Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.320  
   1.321 -ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.322 -        \<Longrightarrow> 
   1.323 -        G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
   1.324 -Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.325 +| ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.326 +          \<Longrightarrow> 
   1.327 +          G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
   1.328 +| Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.329  
   1.330  
   1.331 -LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
   1.332 -       \<Longrightarrow>  
   1.333 -       G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
   1.334 -Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
   1.335 +| LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
   1.336 +         \<Longrightarrow>  
   1.337 +         G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
   1.338 +| Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
   1.339  
   1.340    (* cf. 14.2 *)
   1.341 -CompC1:	"\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.342 -         \<Longrightarrow> 
   1.343 -         G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
   1.344 +| CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.345 +           \<Longrightarrow> 
   1.346 +           G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
   1.347  
   1.348 -Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
   1.349 +| Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
   1.350  
   1.351    (* cf. 14.8.2 *)
   1.352 -IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.353 -      \<Longrightarrow>
   1.354 -      G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
   1.355 -If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
   1.356 -       \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
   1.357 +| IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.358 +        \<Longrightarrow>
   1.359 +        G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
   1.360 +| If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
   1.361 +         \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
   1.362  
   1.363    (* cf. 14.10, 14.10.1 *)
   1.364 -Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
   1.365 -        \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
   1.366 +| Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
   1.367 +          \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
   1.368  
   1.369 -Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
   1.370 +| Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
   1.371  
   1.372 -ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.373 -         \<Longrightarrow>
   1.374 -         G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
   1.375 -Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
   1.376 +| ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
   1.377 +           \<Longrightarrow>
   1.378 +           G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
   1.379 +| Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
   1.380  
   1.381 -TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.382 -        \<Longrightarrow>
   1.383 -        G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
   1.384 -Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
   1.385 -        \<Longrightarrow>
   1.386 -        G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
   1.387 -         \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
   1.388 -                              else (\<langle>Skip\<rangle>,s'))"
   1.389 +| TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.390 +          \<Longrightarrow>
   1.391 +          G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
   1.392 +| Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
   1.393 +          \<Longrightarrow>
   1.394 +          G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
   1.395 +           \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
   1.396 +                                else (\<langle>Skip\<rangle>,s'))"
   1.397  
   1.398 -FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.399 -        \<Longrightarrow>
   1.400 -        G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
   1.401 +| FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
   1.402 +          \<Longrightarrow>
   1.403 +          G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
   1.404  
   1.405 -Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
   1.406 +| Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
   1.407  
   1.408 -FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
   1.409 -        \<Longrightarrow>
   1.410 -        G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
   1.411 -FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
   1.412 +| FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
   1.413 +          \<Longrightarrow>
   1.414 +          G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
   1.415 +| FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
   1.416  
   1.417  
   1.418 -Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
   1.419 -        \<Longrightarrow> 
   1.420 -        G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.421 -Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
   1.422 -       \<Longrightarrow> 
   1.423 -       G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
   1.424 -        \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
   1.425 -              Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
   1.426 -             ,Norm (init_class_obj G C s))"
   1.427 +| Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
   1.428 +          \<Longrightarrow> 
   1.429 +          G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
   1.430 +| Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
   1.431 +         \<Longrightarrow> 
   1.432 +         G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
   1.433 +          \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
   1.434 +                Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
   1.435 +               ,Norm (init_class_obj G C s))"
   1.436  -- {* @{text InsInitE} is just used as trick to embed the statement 
   1.437  @{text "init c"} into an expression*} 
   1.438 -InsInitESKIP:
   1.439 -  "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.440 +| InsInitESKIP:
   1.441 +    "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
   1.442 +
   1.443 +abbreviation
   1.444 +  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
   1.445 +  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^n"
   1.446 +
   1.447 +abbreviation
   1.448 +  steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
   1.449 +  where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*"
   1.450           
   1.451  (* Equivalenzen:
   1.452    Bigstep zu Smallstep komplett.