1(*  Title:      HOL/Bali/Trans.thy
2    Author:     David von Oheimb and Norbert Schirmer
3
4Operational transition (small-step) semantics of the 
5execution of Java expressions and statements
6
7PRELIMINARY!!!!!!!!
8*)
9
10theory Trans imports Evaln begin
11
12definition
13  groundVar :: "var \<Rightarrow> bool" where
14  "groundVar v \<longleftrightarrow> (case v of
15                     LVar ln \<Rightarrow> True
16                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
17                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
18                   | InsInitV c v \<Rightarrow> False)"
19
20lemma groundVar_cases:
21  assumes ground: "groundVar v"
22  obtains (LVar) ln where "v=LVar ln"
23    | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
24    | (AVar) a i where "v=(Lit a).[Lit i]"
25  using ground LVar FVar AVar
26  by (cases v) (auto simp add: groundVar_def)
27
28definition
29  groundExprs :: "expr list \<Rightarrow> bool"
30  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
31  
32primrec the_val:: "expr \<Rightarrow> val"
33  where "the_val (Lit v) = v"
34
35primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
36  "the_var G s (LVar ln) = (lvar ln (store s),s)"
37| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
38| the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
39
40lemma the_var_FVar_simp[simp]:
41"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
42by (simp)
43declare the_var_FVar_def [simp del]
44
45lemma the_var_AVar_simp:
46"the_var G s ((Lit a).[Lit i]) = avar G i a s"
47by (simp)
48declare the_var_AVar_def [simp del]
49
50abbreviation
51  Ref :: "loc \<Rightarrow> expr"
52  where "Ref a == Lit (Addr a)"
53
54abbreviation
55  SKIP :: "expr"
56  where "SKIP == Lit Unit"
57
58inductive
59  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
60  for G :: prog
61where
62
63(* evaluation of expression *)
64  (* cf. 15.5 *)
65  Abrupt:       "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
66                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
67                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
68                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
69                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
70                \<Longrightarrow> 
71                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
72
73| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
74             \<Longrightarrow> 
75             G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
76
77(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
78(* Specialised rules to evaluate: 
79   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
80 
81  (* cf. 15.8.1 *)
82| NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
83| NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
84               \<Longrightarrow> 
85               G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
86
87
88
89(* Alternative when rule SeqE is present 
90NewCInited: "\<lbrakk>inited C (globs s); 
91              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
92             \<Longrightarrow> 
93              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
94
95NewC:
96     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
97     \<Longrightarrow> 
98      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
99
100*)
101  (* cf. 15.9.1 *)
102| NewA: 
103   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
104| InsInitNewAIdx: 
105   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
106    \<Longrightarrow>  
107    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
108| InsInitNewA: 
109   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
110    \<Longrightarrow>
111    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
112 
113  (* cf. 15.15 *)
114| CastE:
115   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
116    \<Longrightarrow>
117    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
118| Cast:
119   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
120    \<Longrightarrow> 
121    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
122  (* can be written without abupd, since we know Norm s *)
123
124
125| InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
126        \<Longrightarrow> 
127        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
128| Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
129          \<Longrightarrow> 
130          G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
131
132  (* cf. 15.7.1 *)
133(*Lit                           "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
134
135| UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
136           \<Longrightarrow> 
137           G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
138| UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
139
140| BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
141             \<Longrightarrow> 
142             G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
143| BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
144             \<Longrightarrow> 
145             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
146              \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
147| BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
148               \<Longrightarrow> 
149               G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
150                \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
151| BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
152              \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
153(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
154   to make the choice between BinOpTerm and BinOp deterministic *)
155   
156| Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
157
158| AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
159          \<Longrightarrow> 
160          G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
161| Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
162         \<Longrightarrow>  
163         G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
164
165(*
166AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
167AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
168          \<Longrightarrow>  
169          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
170           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
171AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
172          \<Longrightarrow>  
173          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
174*) 
175| AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
176           \<Longrightarrow> 
177           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
178| AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
179           \<Longrightarrow> 
180           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
181| Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
182           \<Longrightarrow> 
183           G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
184
185| CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
186          \<Longrightarrow> 
187          G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
188| 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)"
189
190
191| CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
192               \<Longrightarrow>
193               G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
194                \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
195| CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
196               \<Longrightarrow>
197               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
198                \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
199| Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
200                D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
201                s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
202               \<Longrightarrow> 
203               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
204                \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
205           
206| Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
207               \<Longrightarrow> 
208               G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
209
210| CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
211                 \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
212
213| Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
214
215| Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
216
217| InsInitBody: 
218    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
219     \<Longrightarrow> 
220     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
221| InsInitBodyRet: 
222     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
223       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
224
225(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
226  
227| FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
228         \<Longrightarrow> 
229         G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
230          \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
231| InsInitFVarE:
232      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
233       \<Longrightarrow>
234       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
235        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
236| InsInitFVar:
237      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
238        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
239\<comment> \<open>Notice, that we do not have literal values for \<open>vars\<close>. 
240The rules for accessing variables (\<open>Acc\<close>) and assigning to variables 
241(\<open>Ass\<close>), test this with the predicate \<open>groundVar\<close>.  After 
242initialisation is done and the \<open>FVar\<close> is evaluated, we can't just 
243throw away the \<open>InsInitFVar\<close> term and return a literal value, as in the 
244cases of \<open>New\<close>  or \<open>NewC\<close>. Instead we just return the evaluated 
245\<open>FVar\<close> and test for initialisation in the rule \<open>FVar\<close>.\<close>
246
247
248| AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
249           \<Longrightarrow> 
250           G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
251
252| AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
253           \<Longrightarrow> 
254           G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
255
256(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
257
258(* evaluation of expression lists *)
259
260  \<comment> \<open>\<open>Nil\<close>  is fully evaluated\<close>
261
262| ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
263           \<Longrightarrow>
264           G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
265  
266| ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
267           \<Longrightarrow>
268           G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
269
270(* execution of statements *)
271
272  (* cf. 14.5 *)
273| Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
274
275| ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
276          \<Longrightarrow> 
277          G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
278| Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
279
280
281| LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
282         \<Longrightarrow>  
283         G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
284| Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
285
286  (* cf. 14.2 *)
287| CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
288           \<Longrightarrow> 
289           G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
290
291| Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
292
293  (* cf. 14.8.2 *)
294| IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
295        \<Longrightarrow>
296        G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
297| If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
298         \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
299
300  (* cf. 14.10, 14.10.1 *)
301| Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
302          \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
303
304| Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
305
306| ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
307           \<Longrightarrow>
308           G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
309| Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
310
311| TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
312          \<Longrightarrow>
313          G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
314| Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
315          \<Longrightarrow>
316          G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
317           \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
318                                else (\<langle>Skip\<rangle>,s'))"
319
320| FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
321          \<Longrightarrow>
322          G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
323
324| Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
325
326| FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
327          \<Longrightarrow>
328          G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
329| FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
330
331
332| Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
333          \<Longrightarrow> 
334          G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
335| Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
336         \<Longrightarrow> 
337         G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
338          \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
339                Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
340               ,Norm (init_class_obj G C s))"
341\<comment> \<open>\<open>InsInitE\<close> is just used as trick to embed the statement 
342\<open>init c\<close> into an expression\<close> 
343| InsInitESKIP:
344    "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
345
346abbreviation
347  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
348  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
349
350abbreviation
351  steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
352  where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*"
353         
354(* Equivalenzen:
355  Bigstep zu Smallstep komplett.
356  Smallstep zu Bigstep, nur wenn nicht die Ausdr��cke Callee, FinA ,\<dots>
357*)
358
359(*
360lemma imp_eval_trans:
361  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
362    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
363*)
364(* Jetzt muss man bei trans nat��rlich wieder unterscheiden: Stmt, Expr, Var!
365   Sowas bl��des:
366   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
367   the_vals definieren\<dots>
368  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
369*)
370
371
372end
373