src/HOL/Bali/AxSem.thy
changeset 21765 89275a3ed7be
parent 20014 729a45534001
child 23563 42f2f90b51a6
     1.1 --- a/src/HOL/Bali/AxSem.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -435,7 +435,6 @@
     1.4                                                  (   "_\<Turnstile>_:_" [61,0, 58] 57)
     1.5      ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
     1.6                                                  ("_,_|\<Turnstile>_"   [61,58,58] 57)
     1.7 -    ax_derivs :: "prog \<Rightarrow> ('a triples \<times> 'a triples) set"
     1.8  
     1.9  syntax
    1.10  
    1.11 @@ -443,10 +442,6 @@
    1.12                                                  (  "_||=_:_" [61,0, 58] 57)
    1.13       ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
    1.14                                                  ( "_,_|=_"   [61,58,58] 57)
    1.15 -     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
    1.16 -                                                ("_,_||-_"   [61,58,58] 57)
    1.17 -     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
    1.18 -                                                ( "_,_|-_"   [61,58,58] 57)
    1.19  
    1.20  syntax (xsymbols)
    1.21  
    1.22 @@ -454,10 +449,6 @@
    1.23                                                  (  "_|\<Turnstile>_:_" [61,0, 58] 57)
    1.24       ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
    1.25                                                  ( "_,_\<Turnstile>_"   [61,58,58] 57)
    1.26 -     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
    1.27 -                                                ("_,_|\<turnstile>_"   [61,58,58] 57)
    1.28 -     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
    1.29 -                                                ( "_,_\<turnstile>_"   [61,58,58] 57)
    1.30  
    1.31  defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
    1.32                            \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
    1.33 @@ -465,8 +456,6 @@
    1.34  translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
    1.35  defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
    1.36  translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
    1.37 -                     "G,A|\<turnstile>ts" == "(A,ts) \<in> ax_derivs G"
    1.38 -                     "G,A \<turnstile>t"  == "G,A|\<turnstile>{t}"
    1.39  
    1.40  lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
    1.41   (\<forall>Y s Z. P Y s Z 
    1.42 @@ -487,63 +476,69 @@
    1.43  change_claset (fn cs => cs delSWrapper "split_all_tac");
    1.44  *}
    1.45  
    1.46 -inductive "ax_derivs G" intros
    1.47 +inductive2
    1.48 +  ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
    1.49 +  and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
    1.50 +  for G :: prog
    1.51 +where
    1.52  
    1.53 -  empty: " G,A|\<turnstile>{}"
    1.54 -  insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
    1.55 +  "G,A \<turnstile>t \<equiv> G,A|\<turnstile>{t}"
    1.56 +
    1.57 +| empty: " G,A|\<turnstile>{}"
    1.58 +| insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
    1.59            G,A|\<turnstile>insert t ts"
    1.60  
    1.61 -  asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
    1.62 +| asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
    1.63  
    1.64  (* could be added for convenience and efficiency, but is not necessary
    1.65    cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
    1.66             G,A |\<turnstile>ts"
    1.67  *)
    1.68 -  weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
    1.69 +| weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
    1.70  
    1.71 -  conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
    1.72 +| conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
    1.73           (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
    1.74                                   Q  Y' s' Z ))
    1.75                                           \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
    1.76  
    1.77 -  hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
    1.78 +| hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
    1.79  
    1.80 -  Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
    1.81 +| Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
    1.82  
    1.83    --{* variables *}
    1.84 -  LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
    1.85 +| LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
    1.86  
    1.87 -  FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
    1.88 +| FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
    1.89            G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
    1.90                                   G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
    1.91  
    1.92 -  AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
    1.93 +| AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
    1.94            \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
    1.95                                   G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
    1.96    --{* expressions *}
    1.97  
    1.98 -  NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
    1.99 +| NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
   1.100                                   G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
   1.101  
   1.102 -  NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
   1.103 +| NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
   1.104  	  {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
   1.105                                   G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
   1.106  
   1.107 -  Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.108 +| Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.109            abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   1.110                                   G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
   1.111  
   1.112 -  Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.113 +| Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.114                    Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
   1.115                                   G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
   1.116  
   1.117 -  Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
   1.118 +| Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
   1.119  
   1.120 -  UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
   1.121 +| UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
   1.122            \<Longrightarrow>
   1.123            G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
   1.124  
   1.125 -  BinOp:
   1.126 +| BinOp:
   1.127     "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
   1.128       \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
   1.129                 (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
   1.130 @@ -551,20 +546,20 @@
   1.131      \<Longrightarrow>
   1.132      G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
   1.133  
   1.134 -  Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
   1.135 +| Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
   1.136  
   1.137 -  Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   1.138 +| Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   1.139                                   G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
   1.140  
   1.141 -  Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
   1.142 +| Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
   1.143       \<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>
   1.144                                   G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
   1.145  
   1.146 -  Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
   1.147 +| Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
   1.148            \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk> \<Longrightarrow>
   1.149                                   G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
   1.150  
   1.151 -  Call: 
   1.152 +| Call: 
   1.153  "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
   1.154    \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
   1.155   (\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
   1.156 @@ -575,37 +570,37 @@
   1.157   Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
   1.158           G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
   1.159  
   1.160 -  Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
   1.161 +| Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
   1.162                                   G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
   1.163  
   1.164 -  Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
   1.165 +| Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
   1.166    G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
   1.167      \<Longrightarrow>
   1.168                                   G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
   1.169    
   1.170    --{* expression lists *}
   1.171  
   1.172 -  Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
   1.173 +| Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
   1.174  
   1.175 -  Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
   1.176 +| Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
   1.177            \<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
   1.178                                   G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
   1.179  
   1.180    --{* statements *}
   1.181  
   1.182 -  Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
   1.183 +| Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
   1.184  
   1.185 -  Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.186 +| Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.187                                   G,A\<turnstile>{Normal P} .Expr e. {Q}"
   1.188  
   1.189 -  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
   1.190 +| Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
   1.191                             G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
   1.192  
   1.193 -  Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.194 +| Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.195            G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
   1.196                                   G,A\<turnstile>{Normal P} .c1;;c2. {R}"
   1.197  
   1.198 -  If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   1.199 +| If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   1.200            \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
   1.201                                   G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
   1.202  (* unfolding variant of Loop, not needed here
   1.203 @@ -613,28 +608,28 @@
   1.204            \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
   1.205           \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
   1.206  *)
   1.207 -  Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
   1.208 +| Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
   1.209            G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
   1.210                              G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
   1.211    
   1.212 -  Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}"
   1.213 +| Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}"
   1.214  
   1.215 -  Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.216 +| Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.217                                   G,A\<turnstile>{Normal P} .Throw e. {Q}"
   1.218  
   1.219 -  Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
   1.220 +| Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
   1.221            G,A\<turnstile>{Q \<and>. (\<lambda>s.  G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
   1.222                (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
   1.223                                   G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
   1.224  
   1.225 -  Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.226 +| Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.227        \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
   1.228                .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
   1.229                                   G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
   1.230  
   1.231 -  Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
   1.232 +| Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
   1.233  
   1.234 -  Init: "\<lbrakk>the (class G C) = c;
   1.235 +| Init: "\<lbrakk>the (class G C) = c;
   1.236            G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
   1.237                .(if C = Object then Skip else Init (super c)). {Q};
   1.238        \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
   1.239 @@ -645,10 +640,10 @@
   1.240  @{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
   1.241  semantics.
   1.242  *}
   1.243 -  InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
   1.244 -  InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
   1.245 -  Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
   1.246 -  FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
   1.247 +| InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
   1.248 +| InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
   1.249 +| Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
   1.250 +| FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
   1.251  (*
   1.252  axioms 
   1.253  *)
   1.254 @@ -1032,7 +1027,7 @@
   1.255  *}
   1.256  declare ax_Abrupts [intro!]
   1.257  
   1.258 -lemmas ax_Normal_cases = ax_cases [of _ _ normal]
   1.259 +lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
   1.260  
   1.261  lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
   1.262  apply (rule ax_Normal_cases)