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