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