src/HOL/Bali/AxSem.thy

 \item all triples in a derivation are of the same type (due to weak 
       polymorphism)
 \end{itemize}
 *}
 
-
-
 types  res = vals (* result entry *)
 syntax
   Val  :: "val      \<Rightarrow> res"
   Var  :: "var      \<Rightarrow> res"
   Vals :: "val list \<Rightarrow> res"

   (* variables *)
   LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
 
   FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
           G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
-                                 G,A\<turnstile>{Normal P} {C,stat}e..fn=\<succ> {R}"
+                                 G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
 
   AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
           \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
                                  G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
   (* expressions *)

       invC = invocation_class mode (store s) a statT \<and>
          l = locals (store s)) ;.
       init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
       (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
  Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
-         G,A\<turnstile>{Normal P} {statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
+         G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
 
   Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
                                  G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
 
   Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 

   \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
        {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
                      C = invocation_declclass 
                             G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
        G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
-   \<Longrightarrow> G,A\<turnstile>{Normal P} {statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
+   \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
 apply (erule ax_derivs.Call)
 apply  safe
 apply  (erule spec)
 apply (rule ax_escape, clarsimp)
 apply (drule spec, drule spec, drule spec,erule conseq12)

               Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
   G,A\<turnstile>{Normal P} e-\<succ> {Q};
   \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
   \<and>. (\<lambda> s. C=invocation_declclass 
                 G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}
-\<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
+\<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
 apply (erule ax_derivs.Call)
 apply  safe
 apply  (erule spec)
 apply (rule ax_escape, clarsimp)
 apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)