src/HOL/Bali/WellForm.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,3004 @@
     1.4 +(*  Title:      isabelle/Bali/WellForm.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +header {* Well-formedness of Java programs *}
    1.11 +
    1.12 +theory WellForm = WellType:
    1.13 +
    1.14 +text {*
    1.15 +For static checks on expressions and statements, see WellType.thy
    1.16 +
    1.17 +improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
    1.18 +\begin{itemize}
    1.19 +\item a method implementing or overwriting another method may have a result 
    1.20 +      type that widens to the result type of the other method 
    1.21 +      (instead of identical type)
    1.22 +\item if a method hides another method (both methods have to be static!)
    1.23 +  there are no restrictions to the result type 
    1.24 +  since the methods have to be static and there is no dynamic binding of 
    1.25 +  static methods
    1.26 +\item if an interface inherits more than one method with the same signature, the
    1.27 +  methods need not have identical return types
    1.28 +\end{itemize}
    1.29 +simplifications:
    1.30 +\begin{itemize}
    1.31 +\item Object and standard exceptions are assumed to be declared like normal 
    1.32 +      classes
    1.33 +\end{itemize}
    1.34 +*}
    1.35 +
    1.36 +section "well-formed field declarations"
    1.37 +  (* well-formed field declaration (common part for classes and interfaces),
    1.38 +     cf. 8.3 and (9.3) *)
    1.39 +
    1.40 +constdefs
    1.41 +  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
    1.42 + "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
    1.43 +
    1.44 +lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.45 +apply (unfold wf_fdecl_def)
    1.46 +apply simp
    1.47 +done
    1.48 +
    1.49 +
    1.50 +
    1.51 +section "well-formed method declarations"
    1.52 +  (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
    1.53 +  (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
    1.54 +
    1.55 +text {*
    1.56 +A method head is wellformed if:
    1.57 +\begin{itemize}
    1.58 +\item the signature and the method head agree in the number of parameters
    1.59 +\item all types of the parameters are visible
    1.60 +\item the result type is visible
    1.61 +\item the parameter names are unique
    1.62 +\end{itemize} 
    1.63 +*}
    1.64 +constdefs
    1.65 +  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
    1.66 + "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
    1.67 +			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
    1.68 +                            is_acc_type G P (resTy mh) \<and>
    1.69 +			    \<spacespace> nodups (pars mh)"
    1.70 +
    1.71 +
    1.72 +text {*
    1.73 +A method declaration is wellformed if:
    1.74 +\begin{itemize}
    1.75 +\item the method head is wellformed
    1.76 +\item the names of the local variables are unique
    1.77 +\item the types of the local variables must be accessible
    1.78 +\item the local variables don't shadow the parameters
    1.79 +\item the class of the method is defined
    1.80 +\item the body statement is welltyped with respect to the
    1.81 +      modified environment of local names, were the local variables, 
    1.82 +      the parameters the special result variable (Res) and This are assoziated
    1.83 +      with there types. 
    1.84 +\end{itemize}
    1.85 +*}
    1.86 +
    1.87 +constdefs
    1.88 +  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
    1.89 + "wf_mdecl G C \<equiv> 
    1.90 +      \<lambda>(sig,m).
    1.91 +	  wf_mhead G (pid C) sig (mhead m) \<and> 
    1.92 +          unique (lcls (mbody m)) \<and> 
    1.93 +          (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
    1.94 +	  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and>
    1.95 +          is_class G C \<and>
    1.96 +          \<lparr>prg=G,cls=C,
    1.97 +           lcl=\<lambda> k. 
    1.98 +               (case k of
    1.99 +                  EName e 
   1.100 +                  \<Rightarrow> (case e of 
   1.101 +                        VNam v 
   1.102 +                        \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   1.103 +                      | Res \<Rightarrow> Some (resTy m))
   1.104 +	        | This \<Rightarrow> if static m then None else Some (Class C))
   1.105 +          \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>"
   1.106 +
   1.107 +lemma wf_mheadI: 
   1.108 +"\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
   1.109 +  is_acc_type G P (resTy m); nodups (pars m)\<rbrakk> \<Longrightarrow>  
   1.110 +  wf_mhead G P sig m"
   1.111 +apply (unfold wf_mhead_def)
   1.112 +apply (simp (no_asm_simp))
   1.113 +done
   1.114 +
   1.115 +lemma wf_mdeclI: "\<lbrakk>  
   1.116 +  wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
   1.117 +  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 
   1.118 +  \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
   1.119 +  is_class G C;
   1.120 +  \<lparr>prg=G,cls=C,
   1.121 +   lcl=\<lambda> k. 
   1.122 +       (case k of
   1.123 +          EName e 
   1.124 +          \<Rightarrow> (case e of 
   1.125 +                VNam v 
   1.126 +                \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   1.127 +              | Res \<Rightarrow> Some (resTy m))
   1.128 +        | This \<Rightarrow> if static m then None else Some (Class C))
   1.129 +  \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>
   1.130 +  \<rbrakk> \<Longrightarrow>  
   1.131 +  wf_mdecl G C (sig,m)"
   1.132 +apply (unfold wf_mdecl_def)
   1.133 +apply simp
   1.134 +done
   1.135 +
   1.136 +
   1.137 +lemma wf_mdeclD1: 
   1.138 +"wf_mdecl G C (sig,m) \<Longrightarrow>  
   1.139 +   wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and>  
   1.140 +  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 
   1.141 +  (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)"
   1.142 +apply (unfold wf_mdecl_def)
   1.143 +apply auto
   1.144 +done
   1.145 +
   1.146 +lemma wf_mdecl_bodyD: 
   1.147 +"wf_mdecl G C (sig,m) \<Longrightarrow>  
   1.148 + (\<exists>T. \<lparr>prg=G,cls=C,
   1.149 +       lcl = \<lambda> k. 
   1.150 +         (case k of
   1.151 +            EName e 
   1.152 +            \<Rightarrow> (case e of 
   1.153 +                VNam v \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   1.154 +                | Res  \<Rightarrow> Some (resTy m))
   1.155 +          | This \<Rightarrow> if static m then None else Some (Class C))
   1.156 +       \<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> G\<turnstile>T\<preceq>(resTy m))"
   1.157 +apply (unfold wf_mdecl_def)
   1.158 +apply clarify
   1.159 +apply (rule_tac x="(resTy m)" in exI)
   1.160 +apply (unfold wf_mhead_def)
   1.161 +apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
   1.162 +done
   1.163 +
   1.164 +
   1.165 +(*
   1.166 +lemma static_Object_methodsE [elim!]: 
   1.167 + "\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R"
   1.168 +apply (unfold wf_mdecl_def)
   1.169 +apply auto
   1.170 +done
   1.171 +*)
   1.172 +
   1.173 +lemma rT_is_acc_type: 
   1.174 +  "wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)"
   1.175 +apply (unfold wf_mhead_def)
   1.176 +apply auto
   1.177 +done
   1.178 +
   1.179 +section "well-formed interface declarations"
   1.180 +  (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
   1.181 +
   1.182 +text {*
   1.183 +A interface declaration is wellformed if:
   1.184 +\begin{itemize}
   1.185 +\item the interface hierarchy is wellstructured
   1.186 +\item there is no class with the same name
   1.187 +\item the method heads are wellformed and not static and have Public access
   1.188 +\item the methods are uniquely named
   1.189 +\item all superinterfaces are accessible
   1.190 +\item the result type of a method overriding a method of Object widens to the
   1.191 +      result type of the overridden method.
   1.192 +      Shadowing static methods is forbidden.
   1.193 +\item the result type of a method overriding a set of methods defined in the
   1.194 +      superinterfaces widens to each of the corresponding result types
   1.195 +\end{itemize}
   1.196 +*}
   1.197 +constdefs
   1.198 +  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool"
   1.199 + "wf_idecl G \<equiv> 
   1.200 +    \<lambda>(I,i). 
   1.201 +        ws_idecl G I (isuperIfs i) \<and> 
   1.202 +	\<not>is_class G I \<and>
   1.203 +	(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
   1.204 +                                     \<not>is_static mh \<and>
   1.205 +                                      accmodi mh = Public) \<and>
   1.206 +	unique (imethods i) \<and>
   1.207 +        (\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and>
   1.208 +        (table_of (imethods i)
   1.209 +          hiding (methd G Object)
   1.210 +          under  (\<lambda> new old. accmodi old \<noteq> Private)
   1.211 +          entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
   1.212 +                             is_static new = is_static old)) \<and> 
   1.213 +        (o2s \<circ> table_of (imethods i) 
   1.214 +               hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
   1.215 +	       entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
   1.216 +
   1.217 +lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
   1.218 +  wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
   1.219 +apply (unfold wf_idecl_def)
   1.220 +apply auto
   1.221 +done
   1.222 +
   1.223 +lemma wf_idecl_hidings: 
   1.224 +"wf_idecl G (I, i) \<Longrightarrow> 
   1.225 +  (\<lambda>s. o2s (table_of (imethods i) s)) 
   1.226 +  hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
   1.227 +  entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
   1.228 +apply (unfold wf_idecl_def o_def)
   1.229 +apply simp
   1.230 +done
   1.231 +
   1.232 +lemma wf_idecl_hiding:
   1.233 +"wf_idecl G (I, i) \<Longrightarrow> 
   1.234 + (table_of (imethods i)
   1.235 +           hiding (methd G Object)
   1.236 +           under  (\<lambda> new old. accmodi old \<noteq> Private)
   1.237 +           entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
   1.238 +                              is_static new = is_static old))"
   1.239 +apply (unfold wf_idecl_def)
   1.240 +apply simp
   1.241 +done
   1.242 +
   1.243 +lemma wf_idecl_supD: 
   1.244 +"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 
   1.245 + \<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+"
   1.246 +apply (unfold wf_idecl_def ws_idecl_def)
   1.247 +apply auto
   1.248 +done
   1.249 +
   1.250 +section "well-formed class declarations"
   1.251 +  (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
   1.252 +   class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
   1.253 +
   1.254 +text {*
   1.255 +A class declaration is wellformed if:
   1.256 +\begin{itemize}
   1.257 +\item there is no interface with the same name
   1.258 +\item all superinterfaces are accessible and for all methods implementing 
   1.259 +      an interface method the result type widens to the result type of 
   1.260 +      the interface method, the method is not static and offers at least 
   1.261 +      as much access 
   1.262 +      (this actually means that the method has Public access, since all 
   1.263 +      interface methods have public access)
   1.264 +\item all field declarations are wellformed and the field names are unique
   1.265 +\item all method declarations are wellformed and the method names are unique
   1.266 +\item the initialization statement is welltyped
   1.267 +\item the classhierarchy is wellstructured
   1.268 +\item Unless the class is Object:
   1.269 +      \begin{itemize}
   1.270 +      \item the superclass is accessible
   1.271 +      \item for all methods overriding another method (of a superclass )the
   1.272 +            result type widens to the result type of the overridden method,
   1.273 +            the access modifier of the new method provides at least as much
   1.274 +            access as the overwritten one.
   1.275 +      \item for all methods hiding a method (of a superclass) the hidden 
   1.276 +            method must be static and offer at least as much access rights.
   1.277 +            Remark: In contrast to the Java Language Specification we don't
   1.278 +            restrict the result types of the method
   1.279 +            (as in case of overriding), because there seems to be no reason,
   1.280 +            since there is no dynamic binding of static methods.
   1.281 +            (cf. 8.4.6.3 vs. 15.12.1).
   1.282 +            Stricly speaking the restrictions on the access rights aren't 
   1.283 +            necessary to, since the static type and the access rights 
   1.284 +            together determine which method is to be called statically. 
   1.285 +            But if a class gains more then one static method with the 
   1.286 +            same signature due to inheritance, it is confusing when the 
   1.287 +            method selection depends on the access rights only: 
   1.288 +            e.g.
   1.289 +              Class C declares static public method foo().
   1.290 +              Class D is subclass of C and declares static method foo()
   1.291 +              with default package access.
   1.292 +              D.foo() ? if this call is in the same package as D then
   1.293 +                        foo of class D is called, otherwise foo of class C.
   1.294 +      \end{itemize}
   1.295 +
   1.296 +\end{itemize}
   1.297 +*}
   1.298 +(* to Table *)
   1.299 +constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
   1.300 +                                 ("_ entails _" 20)
   1.301 +"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
   1.302 +
   1.303 +lemma entailsD:
   1.304 + "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
   1.305 +by (simp add: entails_def)
   1.306 +
   1.307 +lemma empty_entails[simp]: "empty entails P"
   1.308 +by (simp add: entails_def)
   1.309 +
   1.310 +constdefs
   1.311 + wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
   1.312 +"wf_cdecl G \<equiv> 
   1.313 +   \<lambda>(C,c).
   1.314 +      \<not>is_iface G C \<and>
   1.315 +      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   1.316 +        (\<forall>s. \<forall> im \<in> imethds G I s.
   1.317 +      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
   1.318 +      	                             \<not> is_static cm \<and>
   1.319 +                                     accmodi im \<le> accmodi cm))) \<and>
   1.320 +      (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
   1.321 +      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
   1.322 +      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
   1.323 +      (C \<noteq> Object \<longrightarrow> 
   1.324 +            (is_acc_class G (pid C) (super c) \<and>
   1.325 +            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   1.326 +             entails (\<lambda> new. \<forall> old sig. 
   1.327 +                       (G,sig\<turnstile>new overrides\<^sub>S old 
   1.328 +                        \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
   1.329 +                             accmodi old \<le> accmodi new \<and>
   1.330 +      	                     \<not>is_static old)) \<and>
   1.331 +                       (G,sig\<turnstile>new hides old 
   1.332 +                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   1.333 +      	                      is_static old)))) 
   1.334 +            ))"
   1.335 +
   1.336 +(*
   1.337 +constdefs
   1.338 + wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
   1.339 +"wf_cdecl G \<equiv> 
   1.340 +   \<lambda>(C,c).
   1.341 +      \<not>is_iface G C \<and>
   1.342 +      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   1.343 +        (\<forall>s. \<forall> im \<in> imethds G I s.
   1.344 +      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and>
   1.345 +      	                             \<not> is_static cm \<and>
   1.346 +                                     accmodi im \<le> accmodi cm))) \<and>
   1.347 +      (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
   1.348 +      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
   1.349 +      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
   1.350 +      (C \<noteq> Object \<longrightarrow> 
   1.351 +            (is_acc_class G (pid C) (super c) \<and>
   1.352 +            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   1.353 +              hiding methd G (super c)
   1.354 +              under (\<lambda> new old. G\<turnstile>new overrides old)
   1.355 +              entails (\<lambda> new old. 
   1.356 +                           (G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and>
   1.357 +                            accmodi old \<le> accmodi new \<and>
   1.358 +      	                   \<not> is_static old)))  \<and>
   1.359 +            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   1.360 +              hiding methd G (super c)
   1.361 +              under (\<lambda> new old. G\<turnstile>new hides old)
   1.362 +              entails (\<lambda> new old. is_static old \<and> 
   1.363 +                                  accmodi old \<le> accmodi new))  \<and>
   1.364 +            (table_of (cfields c) hiding accfield G C (super c)
   1.365 +              entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))"
   1.366 +*)
   1.367 +
   1.368 +lemma wf_cdecl_unique: 
   1.369 +"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)"
   1.370 +apply (unfold wf_cdecl_def)
   1.371 +apply auto
   1.372 +done
   1.373 +
   1.374 +lemma wf_cdecl_fdecl: 
   1.375 +"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f"
   1.376 +apply (unfold wf_cdecl_def)
   1.377 +apply auto
   1.378 +done
   1.379 +
   1.380 +lemma wf_cdecl_mdecl: 
   1.381 +"\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m"
   1.382 +apply (unfold wf_cdecl_def)
   1.383 +apply auto
   1.384 +done
   1.385 +
   1.386 +lemma wf_cdecl_impD: 
   1.387 +"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 
   1.388 +\<Longrightarrow> is_acc_iface G (pid C) I \<and>  
   1.389 +    (\<forall>s. \<forall>im \<in> imethds G I s.  
   1.390 +        (\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and>
   1.391 +                                   accmodi im \<le> accmodi cm))"
   1.392 +apply (unfold wf_cdecl_def)
   1.393 +apply auto
   1.394 +done
   1.395 +
   1.396 +lemma wf_cdecl_supD: 
   1.397 +"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow>  
   1.398 +  is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 
   1.399 +   (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   1.400 +    entails (\<lambda> new. \<forall> old sig. 
   1.401 +                 (G,sig\<turnstile>new overrides\<^sub>S old 
   1.402 +                  \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
   1.403 +                       accmodi old \<le> accmodi new \<and>
   1.404 +                       \<not>is_static old)) \<and>
   1.405 +                 (G,sig\<turnstile>new hides old 
   1.406 +                   \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   1.407 +                        is_static old))))"
   1.408 +apply (unfold wf_cdecl_def ws_cdecl_def)
   1.409 +apply auto
   1.410 +done
   1.411 +
   1.412 +
   1.413 +lemma wf_cdecl_overrides_SomeD:
   1.414 +"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
   1.415 +  G,sig\<turnstile>(C,newM) overrides\<^sub>S old
   1.416 +\<rbrakk> \<Longrightarrow>  G\<turnstile>resTy newM\<preceq>resTy old \<and>
   1.417 +       accmodi old \<le> accmodi newM \<and>
   1.418 +       \<not> is_static old" 
   1.419 +apply (drule (1) wf_cdecl_supD)
   1.420 +apply (clarify)
   1.421 +apply (drule entailsD)
   1.422 +apply   (blast intro: table_of_map_SomeI)
   1.423 +apply (drule_tac x="old" in spec)
   1.424 +apply (auto dest: overrides_eq_sigD simp add: msig_def)
   1.425 +done
   1.426 +
   1.427 +lemma wf_cdecl_hides_SomeD:
   1.428 +"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
   1.429 +  G,sig\<turnstile>(C,newM) hides old
   1.430 +\<rbrakk> \<Longrightarrow>  accmodi old \<le> access newM \<and>
   1.431 +       is_static old" 
   1.432 +apply (drule (1) wf_cdecl_supD)
   1.433 +apply (clarify)
   1.434 +apply (drule entailsD)
   1.435 +apply   (blast intro: table_of_map_SomeI)
   1.436 +apply (drule_tac x="old" in spec)
   1.437 +apply (auto dest: hides_eq_sigD simp add: msig_def)
   1.438 +done
   1.439 +
   1.440 +lemma wf_cdecl_wt_init: 
   1.441 + "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
   1.442 +apply (unfold wf_cdecl_def)
   1.443 +apply auto
   1.444 +done
   1.445 +
   1.446 +
   1.447 +section "well-formed programs"
   1.448 +  (* well-formed program, cf. 8.1, 9.1 *)
   1.449 +
   1.450 +text {*
   1.451 +A program declaration is wellformed if:
   1.452 +\begin{itemize}
   1.453 +\item the class ObjectC of Object is defined
   1.454 +\item every method of has an access modifier distinct from Package. This is
   1.455 +      necessary since every interface automatically inherits from Object.  
   1.456 +      We must know, that every time a Object method is "overriden" by an 
   1.457 +      interface method this is also overriden by the class implementing the
   1.458 +      the interface (see @{text "implement_dynmethd and class_mheadsD"})
   1.459 +\item all standard Exceptions are defined
   1.460 +\item all defined interfaces are wellformed
   1.461 +\item all defined classes are wellformed
   1.462 +\end{itemize}
   1.463 +*}
   1.464 +constdefs
   1.465 +  wf_prog  :: "prog \<Rightarrow> bool"
   1.466 + "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
   1.467 +	         ObjectC \<in> set cs \<and> 
   1.468 +                (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
   1.469 +                (\<forall>xn. SXcptC xn \<in> set cs) \<and>
   1.470 +		(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
   1.471 +		(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
   1.472 +
   1.473 +lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
   1.474 +apply (unfold wf_prog_def Let_def)
   1.475 +apply simp
   1.476 +apply (fast dest: map_of_SomeD)
   1.477 +done
   1.478 +
   1.479 +lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)"
   1.480 +apply (unfold wf_prog_def Let_def)
   1.481 +apply simp
   1.482 +apply (fast dest: map_of_SomeD)
   1.483 +done
   1.484 +
   1.485 +lemma wf_prog_Object_mdecls:
   1.486 +"wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)"
   1.487 +apply (unfold wf_prog_def Let_def)
   1.488 +apply simp
   1.489 +done
   1.490 +
   1.491 +lemma wf_prog_acc_superD:
   1.492 + "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 
   1.493 +  \<Longrightarrow> is_acc_class G (pid C) (super c)"
   1.494 +by (auto dest: wf_prog_cdecl wf_cdecl_supD)
   1.495 +
   1.496 +lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G"
   1.497 +apply (unfold wf_prog_def Let_def)
   1.498 +apply (rule ws_progI)
   1.499 +apply  (simp_all (no_asm))
   1.500 +apply  (auto simp add: is_acc_class_def is_acc_iface_def 
   1.501 +             dest!: wf_idecl_supD wf_cdecl_supD )+
   1.502 +done
   1.503 +
   1.504 +lemma class_Object [simp]: 
   1.505 +"wf_prog G \<Longrightarrow> 
   1.506 +  class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
   1.507 +                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>"
   1.508 +apply (unfold wf_prog_def Let_def ObjectC_def)
   1.509 +apply (fast dest!: map_of_SomeI)
   1.510 +done
   1.511 +
   1.512 +lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object =  
   1.513 +  table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)"
   1.514 +apply (subst methd_rec)
   1.515 +apply (auto simp add: Let_def)
   1.516 +done
   1.517 +
   1.518 +lemma wf_prog_Object_methd:
   1.519 +"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package"
   1.520 +by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 
   1.521 +
   1.522 +lemma wf_prog_Object_is_public[intro]:
   1.523 + "wf_prog G \<Longrightarrow> is_public G Object"
   1.524 +by (auto simp add: is_public_def dest: class_Object)
   1.525 +
   1.526 +lemma class_SXcpt [simp]: 
   1.527 +"wf_prog G \<Longrightarrow> 
   1.528 +  class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   1.529 +                                   init=Skip,
   1.530 +                                   super=if xn = Throwable then Object 
   1.531 +                                                           else SXcpt Throwable,
   1.532 +                                   superIfs=[]\<rparr>"
   1.533 +apply (unfold wf_prog_def Let_def SXcptC_def)
   1.534 +apply (fast dest!: map_of_SomeI)
   1.535 +done
   1.536 +
   1.537 +lemma wf_ObjectC [simp]: 
   1.538 +	"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls)
   1.539 +  (wf_mdecl G Object) \<and> unique Object_mdecls)"
   1.540 +apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
   1.541 +apply (simp (no_asm))
   1.542 +done
   1.543 +
   1.544 +lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object"
   1.545 +apply (simp (no_asm_simp))
   1.546 +done
   1.547 + 
   1.548 +lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object"
   1.549 +apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
   1.550 +                               accessible_in_RefT_simp)
   1.551 +done
   1.552 +
   1.553 +lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)"
   1.554 +apply (simp (no_asm_simp))
   1.555 +done
   1.556 +
   1.557 +lemma SXcpt_is_acc_class [simp,elim!]: 
   1.558 +"wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)"
   1.559 +apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
   1.560 +                               accessible_in_RefT_simp)
   1.561 +done
   1.562 +
   1.563 +lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []"
   1.564 +by (force intro: fields_emptyI)
   1.565 +
   1.566 +lemma accfield_Object [simp]: 
   1.567 + "wf_prog G \<Longrightarrow> accfield G S Object = empty"
   1.568 +apply (unfold accfield_def)
   1.569 +apply (simp (no_asm_simp) add: Let_def)
   1.570 +done
   1.571 +
   1.572 +lemma fields_Throwable [simp]: 
   1.573 + "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []"
   1.574 +by (force intro: fields_emptyI)
   1.575 +
   1.576 +lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []"
   1.577 +apply (case_tac "xn = Throwable")
   1.578 +apply  (simp (no_asm_simp))
   1.579 +by (force intro: fields_emptyI)
   1.580 +
   1.581 +lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim]
   1.582 +lemma widen_trans2 [elim]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.583 +apply (erule (2) widen_trans)
   1.584 +done
   1.585 +
   1.586 +lemma Xcpt_subcls_Throwable [simp]: 
   1.587 +"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
   1.588 +apply (rule SXcpt_subcls_Throwable_lemma)
   1.589 +apply auto
   1.590 +done
   1.591 +
   1.592 +lemma unique_fields: 
   1.593 + "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)"
   1.594 +apply (erule ws_unique_fields)
   1.595 +apply  (erule wf_ws_prog)
   1.596 +apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
   1.597 +done
   1.598 +
   1.599 +lemma fields_mono: 
   1.600 +"\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 
   1.601 +  is_class G D; wf_prog G\<rbrakk> 
   1.602 +   \<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f"
   1.603 +apply (rule map_of_SomeI)
   1.604 +apply  (erule (1) unique_fields)
   1.605 +apply (erule (1) map_of_SomeD [THEN fields_mono_lemma])
   1.606 +apply (erule wf_ws_prog)
   1.607 +done
   1.608 +
   1.609 +
   1.610 +lemma fields_is_type [elim]: 
   1.611 +"\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   1.612 +      is_type G (type f)"
   1.613 +apply (frule wf_ws_prog)
   1.614 +apply (force dest: fields_declC [THEN conjunct1] 
   1.615 +                   wf_prog_cdecl [THEN wf_cdecl_fdecl]
   1.616 +             simp add: wf_fdecl_def2 is_acc_type_def)
   1.617 +done
   1.618 +
   1.619 +lemma imethds_wf_mhead [rule_format (no_asm)]: 
   1.620 +"\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow>  
   1.621 +  wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 
   1.622 +  \<not> is_static m \<and> accmodi m = Public"
   1.623 +apply (frule wf_ws_prog)
   1.624 +apply (drule (2) imethds_declI [THEN conjunct1])
   1.625 +apply clarify
   1.626 +apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption)
   1.627 +apply (drule wf_idecl_mhead)
   1.628 +apply (erule map_of_SomeD)
   1.629 +apply (cases m, simp)
   1.630 +done
   1.631 +
   1.632 +lemma methd_wf_mdecl: 
   1.633 + "\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow>  
   1.634 +  G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 
   1.635 +  wf_mdecl G (declclass m) (sig,(mthd m))"
   1.636 +apply (frule wf_ws_prog)
   1.637 +apply (drule (1) methd_declC)
   1.638 +apply  fast
   1.639 +apply clarsimp
   1.640 +apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
   1.641 +done
   1.642 +
   1.643 +(*
   1.644 +This lemma doesn't hold!
   1.645 +lemma methd_rT_is_acc_type: 
   1.646 +"\<lbrakk>wf_prog G;methd G C C sig = Some (D,m);
   1.647 +    class G C = Some y\<rbrakk>
   1.648 +\<Longrightarrow> is_acc_type G (pid C) (resTy m)"
   1.649 +The result Type is only visible in the scope of defining class D 
   1.650 +"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C!
   1.651 +(The same is true for the type of pramaters of a method)
   1.652 +*)
   1.653 +
   1.654 +
   1.655 +lemma methd_rT_is_type: 
   1.656 +"\<lbrakk>wf_prog G;methd G C sig = Some m;
   1.657 +    class G C = Some y\<rbrakk>
   1.658 +\<Longrightarrow> is_type G (resTy m)"
   1.659 +apply (drule (2) methd_wf_mdecl)
   1.660 +apply clarify
   1.661 +apply (drule wf_mdeclD1)
   1.662 +apply clarify
   1.663 +apply (drule rT_is_acc_type)
   1.664 +apply (cases m, simp add: is_acc_type_def)
   1.665 +done
   1.666 +
   1.667 +lemma accmethd_rT_is_type:
   1.668 +"\<lbrakk>wf_prog G;accmethd G S C sig = Some m;
   1.669 +    class G C = Some y\<rbrakk>
   1.670 +\<Longrightarrow> is_type G (resTy m)"
   1.671 +by (auto simp add: accmethd_def  
   1.672 +         intro: methd_rT_is_type)
   1.673 +
   1.674 +lemma methd_Object_SomeD:
   1.675 +"\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 
   1.676 + \<Longrightarrow> declclass m = Object"
   1.677 +by (auto dest: class_Object simp add: methd_rec )
   1.678 +
   1.679 +lemma wf_imethdsD: 
   1.680 + "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
   1.681 + \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
   1.682 +proof -
   1.683 +  assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
   1.684 +  have "wf_prog G \<longrightarrow> 
   1.685 +         (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
   1.686 +                  \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
   1.687 +  proof (rule iface_rec.induct,intro allI impI)
   1.688 +    fix G I i im
   1.689 +    assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
   1.690 +                 \<longrightarrow> ?P G J"
   1.691 +    assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
   1.692 +           im: "im \<in> imethds G I sig" 
   1.693 +    show "\<not>is_static im \<and> accmodi im = Public" 
   1.694 +    proof -
   1.695 +      let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
   1.696 +      let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
   1.697 +      from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
   1.698 +	by (simp add: imethds_rec)
   1.699 +      from wf if_I have 
   1.700 +	wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)"
   1.701 +	by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
   1.702 +      from wf if_I have
   1.703 +	"\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public"
   1.704 +	by (auto dest!: wf_prog_idecl wf_idecl_mhead)
   1.705 +      then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
   1.706 +                         \<longrightarrow>  \<not> is_static im \<and> accmodi im = Public"
   1.707 +	by (auto dest!: table_of_Some_in_set)
   1.708 +      show ?thesis
   1.709 +	proof (cases "?new sig = {}")
   1.710 +	  case True
   1.711 +	  from True wf wf_supI if_I imethds hyp 
   1.712 +	  show ?thesis by (auto simp del:  split_paired_All)  
   1.713 +	next
   1.714 +	  case False
   1.715 +	  from False wf wf_supI if_I imethds new_ok hyp 
   1.716 +	  show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
   1.717 +	qed
   1.718 +      qed
   1.719 +    qed
   1.720 +  with asm show ?thesis by (auto simp del: split_paired_All)
   1.721 +qed
   1.722 +
   1.723 +lemma wf_prog_hidesD:
   1.724 + (assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G") 
   1.725 +   "accmodi old \<le> accmodi new \<and>
   1.726 +    is_static old"
   1.727 +proof -
   1.728 +  from hides 
   1.729 +  obtain c where 
   1.730 +    clsNew: "class G (declclass new) = Some c" and
   1.731 +    neqObj: "declclass new \<noteq> Object"
   1.732 +    by (auto dest: hidesD declared_in_classD)
   1.733 +  with hides obtain newM oldM where
   1.734 +    newM: "table_of (methods c) (msig new) = Some newM" and 
   1.735 +     new: "new = (declclass new,(msig new),newM)" and
   1.736 +     old: "old = (declclass old,(msig old),oldM)" and
   1.737 +          "msig new = msig old"
   1.738 +    by (cases new,cases old) 
   1.739 +       (auto dest: hidesD 
   1.740 +         simp add: cdeclaredmethd_def declared_in_def)
   1.741 +  with hides 
   1.742 +  have hides':
   1.743 +        "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)"
   1.744 +    by auto
   1.745 +  from clsNew wf 
   1.746 +  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   1.747 +  note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
   1.748 +  with new old 
   1.749 +  show ?thesis
   1.750 +    by (cases new, cases old) auto
   1.751 +qed
   1.752 +
   1.753 +text {* Compare this lemma about static  
   1.754 +overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 
   1.755 +dynamic overriding @{term "G \<turnstile>new overrides old"}. 
   1.756 +Conforming result types and restrictions on the access modifiers of the old 
   1.757 +and the new method are not part of the predicate for static overriding. But
   1.758 +they are enshured in a wellfromed program.  Dynamic overriding has 
   1.759 +no restrictions on the access modifiers but enforces confrom result types 
   1.760 +as precondition. But with some efford we can guarantee the access modifier
   1.761 +restriction for dynamic overriding, too. See lemma 
   1.762 +@{text wf_prog_dyn_override_prop}.
   1.763 +*}
   1.764 +lemma wf_prog_stat_overridesD:
   1.765 + (assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G") 
   1.766 +   "G\<turnstile>resTy new\<preceq>resTy old \<and>
   1.767 +    accmodi old \<le> accmodi new \<and>
   1.768 +    \<not> is_static old"
   1.769 +proof -
   1.770 +  from stat_override 
   1.771 +  obtain c where 
   1.772 +    clsNew: "class G (declclass new) = Some c" and
   1.773 +    neqObj: "declclass new \<noteq> Object"
   1.774 +    by (auto dest: stat_overrides_commonD declared_in_classD)
   1.775 +  with stat_override obtain newM oldM where
   1.776 +    newM: "table_of (methods c) (msig new) = Some newM" and 
   1.777 +     new: "new = (declclass new,(msig new),newM)" and
   1.778 +     old: "old = (declclass old,(msig old),oldM)" and
   1.779 +          "msig new = msig old"
   1.780 +    by (cases new,cases old) 
   1.781 +       (auto dest: stat_overrides_commonD 
   1.782 +         simp add: cdeclaredmethd_def declared_in_def)
   1.783 +  with stat_override 
   1.784 +  have stat_override':
   1.785 +        "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
   1.786 +    by auto
   1.787 +  from clsNew wf 
   1.788 +  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   1.789 +  note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
   1.790 +  with new old 
   1.791 +  show ?thesis
   1.792 +    by (cases new, cases old) auto
   1.793 +qed
   1.794 +    
   1.795 +lemma static_to_dynamic_overriding: 
   1.796 +  (assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G")
   1.797 +   "G\<turnstile>new overrides old"
   1.798 +proof -
   1.799 +  from stat_override 
   1.800 +  show ?thesis (is "?Overrides new old")
   1.801 +  proof (induct)
   1.802 +    case (Direct new old superNew)
   1.803 +    then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 
   1.804 +      by (rule stat_overridesR.Direct)
   1.805 +    from stat_override wf
   1.806 +    have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and
   1.807 +      not_static_old: "\<not> is_static old" 
   1.808 +      by (auto dest: wf_prog_stat_overridesD)  
   1.809 +    have not_private_new: "accmodi new \<noteq> Private"
   1.810 +    proof -
   1.811 +      from stat_override 
   1.812 +      have "accmodi old \<noteq> Private"
   1.813 +	by (rule no_Private_stat_override)
   1.814 +      moreover
   1.815 +      from stat_override wf
   1.816 +      have "accmodi old \<le> accmodi new"
   1.817 +	by (auto dest: wf_prog_stat_overridesD)
   1.818 +      ultimately
   1.819 +      show ?thesis
   1.820 +	by (auto dest: acc_modi_bottom)
   1.821 +    qed
   1.822 +    with Direct resTy_widen not_static_old 
   1.823 +    show "?Overrides new old" 
   1.824 +      by (auto intro: overridesR.Direct) 
   1.825 +  next
   1.826 +    case (Indirect inter new old)
   1.827 +    then show "?Overrides new old" 
   1.828 +      by (blast intro: overridesR.Indirect) 
   1.829 +  qed
   1.830 +qed
   1.831 +
   1.832 +lemma non_Package_instance_method_inheritance:
   1.833 +(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
   1.834 +             accmodi_old: "accmodi old \<noteq> Package" and 
   1.835 +         instance_method: "\<not> is_static old" and
   1.836 +                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
   1.837 +            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
   1.838 +                      wf: "wf_prog G"
   1.839 +) "G\<turnstile>Method old member_of C \<or>
   1.840 +   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and>  G\<turnstile>Method new member_of C)"
   1.841 +proof -
   1.842 +  from wf have ws: "ws_prog G" by auto
   1.843 +  from old_declared have iscls_declC_old: "is_class G (declclass old)"
   1.844 +    by (auto simp add: declared_in_def cdeclaredmethd_def)
   1.845 +  from subcls have  iscls_C: "is_class G C"
   1.846 +    by (blast dest:  subcls_is_class)
   1.847 +  from iscls_C ws old_inheritable subcls 
   1.848 +  show ?thesis (is "?P C old")
   1.849 +  proof (induct rule: ws_class_induct')
   1.850 +    case Object
   1.851 +    assume "G\<turnstile>Object\<prec>\<^sub>C declclass old"
   1.852 +    then show "?P Object old"
   1.853 +      by blast
   1.854 +  next
   1.855 +    case (Subcls C c)
   1.856 +    assume cls_C: "class G C = Some c" and 
   1.857 +       neq_C_Obj: "C \<noteq> Object" and
   1.858 +             hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 
   1.859 +                   G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and
   1.860 +     inheritable: "G \<turnstile>Method old inheritable_in pid C" and
   1.861 +         subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
   1.862 +    from cls_C neq_C_Obj  
   1.863 +    have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 
   1.864 +      by (rule subcls1I)
   1.865 +    from wf cls_C neq_C_Obj
   1.866 +    have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
   1.867 +      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
   1.868 +    {
   1.869 +      fix old
   1.870 +      assume    member_super: "G\<turnstile>Method old member_of (super c)"
   1.871 +      assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
   1.872 +      assume instance_method: "\<not> is_static old"
   1.873 +      from member_super
   1.874 +      have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
   1.875 +       by (cases old) (auto dest: member_of_declC)
   1.876 +      have "?P C old"
   1.877 +      proof (cases "G\<turnstile>mid (msig old) undeclared_in C")
   1.878 +	case True
   1.879 +	with inheritable super accessible_super member_super
   1.880 +	have "G\<turnstile>Method old member_of C"
   1.881 +	  by (cases old) (auto intro: members.Inherited)
   1.882 +	then show ?thesis
   1.883 +	  by auto
   1.884 +      next
   1.885 +	case False
   1.886 +	then obtain new_member where
   1.887 +	     "G\<turnstile>new_member declared_in C" and
   1.888 +             "mid (msig old) = memberid new_member"
   1.889 +          by (auto dest: not_undeclared_declared)
   1.890 +	then obtain new where
   1.891 +	          new: "G\<turnstile>Method new declared_in C" and
   1.892 +               eq_sig: "msig old = msig new" and
   1.893 +	    declC_new: "declclass new = C" 
   1.894 +	  by (cases new_member) auto
   1.895 +	then have member_new: "G\<turnstile>Method new member_of C"
   1.896 +	  by (cases new) (auto intro: members.Immediate)
   1.897 +	from declC_new super member_super
   1.898 +	have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
   1.899 +	  by (auto dest!: member_of_subclseq_declC
   1.900 +	            dest: r_into_trancl intro: trancl_rtrancl_trancl)
   1.901 +	show ?thesis
   1.902 +	proof (cases "is_static new")
   1.903 +	  case False
   1.904 +	  with eq_sig declC_new new old_declared inheritable
   1.905 +	       super member_super subcls_new_old
   1.906 +	  have "G\<turnstile>new overrides\<^sub>S old"
   1.907 +	    by (auto intro!: stat_overridesR.Direct)
   1.908 +	  with member_new show ?thesis
   1.909 +	    by blast
   1.910 +	next
   1.911 +	  case True
   1.912 +	  with eq_sig declC_new subcls_new_old new old_declared inheritable
   1.913 +	  have "G\<turnstile>new hides old"
   1.914 +	    by (auto intro: hidesI)    
   1.915 +	  with wf 
   1.916 +	  have "is_static old"
   1.917 +	    by (blast dest: wf_prog_hidesD)
   1.918 +	  with instance_method
   1.919 +	  show ?thesis
   1.920 +	    by (contradiction)
   1.921 +	qed
   1.922 +      qed
   1.923 +    } note hyp_member_super = this
   1.924 +    from subclsC cls_C 
   1.925 +    have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
   1.926 +      by (rule subcls_superD)
   1.927 +    then
   1.928 +    show "?P C old"
   1.929 +    proof (cases rule: subclseq_cases) 
   1.930 +      case Eq
   1.931 +      assume "super c = declclass old"
   1.932 +      with old_declared 
   1.933 +      have "G\<turnstile>Method old member_of (super c)" 
   1.934 +	by (cases old) (auto intro: members.Immediate)
   1.935 +      with inheritable instance_method 
   1.936 +      show ?thesis
   1.937 +	by (blast dest: hyp_member_super)
   1.938 +    next
   1.939 +      case Subcls
   1.940 +      assume "G\<turnstile>super c\<prec>\<^sub>C declclass old"
   1.941 +      moreover
   1.942 +      from inheritable accmodi_old
   1.943 +      have "G \<turnstile>Method old inheritable_in pid (super c)"
   1.944 +	by (cases "accmodi old") (auto simp add: inheritable_in_def)
   1.945 +      ultimately
   1.946 +      have "?P (super c) old"
   1.947 +	by (blast dest: hyp)
   1.948 +      then show ?thesis
   1.949 +      proof
   1.950 +	assume "G \<turnstile>Method old member_of super c"
   1.951 +	with inheritable instance_method
   1.952 +	show ?thesis
   1.953 +	  by (blast dest: hyp_member_super)
   1.954 +      next
   1.955 +	assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c"
   1.956 +	then obtain super_new where
   1.957 +	  super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
   1.958 +            super_new_member:  "G \<turnstile>Method super_new member_of super c"
   1.959 +	  by blast
   1.960 +	from super_new_override wf
   1.961 +	have "accmodi old \<le> accmodi super_new"
   1.962 +	  by (auto dest: wf_prog_stat_overridesD)
   1.963 +	with inheritable accmodi_old
   1.964 +	have "G \<turnstile>Method super_new inheritable_in pid C"
   1.965 +	  by (auto simp add: inheritable_in_def 
   1.966 +	              split: acc_modi.splits
   1.967 +                       dest: acc_modi_le_Dests)
   1.968 +	moreover
   1.969 +	from super_new_override 
   1.970 +	have "\<not> is_static super_new"
   1.971 +	  by (auto dest: stat_overrides_commonD)
   1.972 +	moreover
   1.973 +	note super_new_member
   1.974 +	ultimately have "?P C super_new"
   1.975 +	  by (auto dest: hyp_member_super)
   1.976 +	then show ?thesis
   1.977 +	proof 
   1.978 +	  assume "G \<turnstile>Method super_new member_of C"
   1.979 +	  with super_new_override
   1.980 +	  show ?thesis
   1.981 +	    by blast
   1.982 +	next
   1.983 +	  assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
   1.984 +                  G \<turnstile>Method new member_of C"
   1.985 +	  with super_new_override show ?thesis
   1.986 +	    by (blast intro: stat_overridesR.Indirect) 
   1.987 +	qed
   1.988 +      qed
   1.989 +    qed
   1.990 +  qed
   1.991 +qed
   1.992 +
   1.993 +lemma non_Package_instance_method_inheritance_cases [consumes 6,
   1.994 +         case_names Inheritance Overriding]:
   1.995 +(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
   1.996 +             accmodi_old: "accmodi old \<noteq> Package" and 
   1.997 +         instance_method: "\<not> is_static old" and
   1.998 +                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
   1.999 +            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
  1.1000 +                      wf: "wf_prog G" and
  1.1001 +             inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
  1.1002 +             overriding:  "\<And> new. 
  1.1003 +                           \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
  1.1004 +                           \<Longrightarrow> P"
  1.1005 +) "P"
  1.1006 +proof -
  1.1007 +  from old_inheritable accmodi_old instance_method subcls old_declared wf 
  1.1008 +       inheritance overriding
  1.1009 +  show ?thesis
  1.1010 +    by (auto dest: non_Package_instance_method_inheritance)
  1.1011 +qed
  1.1012 +
  1.1013 +lemma dynamic_to_static_overriding:
  1.1014 +(assumes dyn_override: "G\<turnstile> new overrides old" and
  1.1015 +          accmodi_old: "accmodi old \<noteq> Package" and
  1.1016 +                   wf: "wf_prog G"
  1.1017 +) "G\<turnstile> new overrides\<^sub>S old"  
  1.1018 +proof - 
  1.1019 +  from dyn_override accmodi_old
  1.1020 +  show ?thesis (is "?Overrides new old")
  1.1021 +  proof (induct rule: overridesR.induct)
  1.1022 +    case (Direct new old)
  1.1023 +    assume   new_declared: "G\<turnstile>Method new declared_in declclass new"
  1.1024 +    assume eq_sig_new_old: "msig new = msig old"
  1.1025 +    assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
  1.1026 +    assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and
  1.1027 +           "accmodi old \<noteq> Package" and
  1.1028 +           "\<not> is_static old" and
  1.1029 +           "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and
  1.1030 +           "G\<turnstile>Method old declared_in declclass old" 
  1.1031 +    from this wf
  1.1032 +    show "?Overrides new old"
  1.1033 +    proof (cases rule: non_Package_instance_method_inheritance_cases)
  1.1034 +      case Inheritance
  1.1035 +      assume "G \<turnstile>Method old member_of declclass new"
  1.1036 +      then have "G\<turnstile>mid (msig old) undeclared_in declclass new"
  1.1037 +      proof cases
  1.1038 +	case Immediate 
  1.1039 +	with subcls_new_old wf show ?thesis 	
  1.1040 +	  by (auto dest: subcls_irrefl)
  1.1041 +      next
  1.1042 +	case Inherited
  1.1043 +	then show ?thesis
  1.1044 +	  by (cases old) auto
  1.1045 +      qed
  1.1046 +      with eq_sig_new_old new_declared
  1.1047 +      show ?thesis
  1.1048 +	by (cases old,cases new) (auto dest!: declared_not_undeclared)
  1.1049 +    next
  1.1050 +      case (Overriding new') 
  1.1051 +      assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old"
  1.1052 +      then have "msig new' = msig old"
  1.1053 +	by (auto dest: stat_overrides_commonD)
  1.1054 +      with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
  1.1055 +	by simp
  1.1056 +      assume "G \<turnstile>Method new' member_of declclass new"
  1.1057 +      then show ?thesis
  1.1058 +      proof (cases)
  1.1059 +	case Immediate
  1.1060 +	then have declC_new: "declclass new' = declclass new" 
  1.1061 +	  by auto
  1.1062 +	from Immediate 
  1.1063 +	have "G\<turnstile>Method new' declared_in declclass new"
  1.1064 +	  by (cases new') auto
  1.1065 +	with new_declared eq_sig_new_new' declC_new 
  1.1066 +	have "new=new'"
  1.1067 +	  by (cases new, cases new') (auto dest: unique_declared_in) 
  1.1068 +	with stat_override_new'
  1.1069 +	show ?thesis
  1.1070 +	  by simp
  1.1071 +      next
  1.1072 +	case Inherited
  1.1073 +	then have "G\<turnstile>mid (msig new') undeclared_in declclass new"
  1.1074 +	  by (cases new') (auto)
  1.1075 +	with eq_sig_new_new' new_declared
  1.1076 +	show ?thesis
  1.1077 +	  by (cases new,cases new') (auto dest!: declared_not_undeclared)
  1.1078 +      qed
  1.1079 +    qed
  1.1080 +  next
  1.1081 +    case (Indirect inter new old)
  1.1082 +    assume accmodi_old: "accmodi old \<noteq> Package"
  1.1083 +    assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old"
  1.1084 +    with accmodi_old 
  1.1085 +    have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old"
  1.1086 +      by blast
  1.1087 +    moreover 
  1.1088 +    assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter"
  1.1089 +    moreover
  1.1090 +    have "accmodi inter \<noteq> Package"
  1.1091 +    proof -
  1.1092 +      from stat_override_inter_old wf 
  1.1093 +      have "accmodi old \<le> accmodi inter"
  1.1094 +	by (auto dest: wf_prog_stat_overridesD)
  1.1095 +      with stat_override_inter_old accmodi_old
  1.1096 +      show ?thesis
  1.1097 +	by (auto dest!: no_Private_stat_override
  1.1098 +                 split: acc_modi.splits 
  1.1099 +	         dest: acc_modi_le_Dests)
  1.1100 +    qed
  1.1101 +    ultimately show "?Overrides new old"
  1.1102 +      by (blast intro: stat_overridesR.Indirect)
  1.1103 +  qed
  1.1104 +qed
  1.1105 +
  1.1106 +lemma wf_prog_dyn_override_prop:
  1.1107 + (assumes dyn_override: "G \<turnstile> new overrides old" and
  1.1108 +                    wf: "wf_prog G"
  1.1109 + ) "accmodi old \<le> accmodi new"
  1.1110 +proof (cases "accmodi old = Package")
  1.1111 +  case True
  1.1112 +  note old_Package = this
  1.1113 +  show ?thesis
  1.1114 +  proof (cases "accmodi old \<le> accmodi new")
  1.1115 +    case True then show ?thesis .
  1.1116 +  next
  1.1117 +    case False
  1.1118 +    with old_Package 
  1.1119 +    have "accmodi new = Private"
  1.1120 +      by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
  1.1121 +    with dyn_override 
  1.1122 +    show ?thesis
  1.1123 +      by (auto dest: overrides_commonD)
  1.1124 +  qed    
  1.1125 +next
  1.1126 +  case False
  1.1127 +  with dyn_override wf
  1.1128 +  have "G \<turnstile> new overrides\<^sub>S old"
  1.1129 +    by (blast intro: dynamic_to_static_overriding)
  1.1130 +  with wf 
  1.1131 +  show ?thesis
  1.1132 +   by (blast dest: wf_prog_stat_overridesD)
  1.1133 +qed 
  1.1134 +
  1.1135 +lemma overrides_Package_old: 
  1.1136 +(assumes dyn_override: "G \<turnstile> new overrides old" and 
  1.1137 +          accmodi_new: "accmodi new = Package" and
  1.1138 +                   wf: "wf_prog G "
  1.1139 +) "accmodi old = Package"
  1.1140 +proof (cases "accmodi old")
  1.1141 +  case Private
  1.1142 +  with dyn_override show ?thesis
  1.1143 +    by (simp add: no_Private_override)
  1.1144 +next
  1.1145 +  case Package
  1.1146 +  then show ?thesis .
  1.1147 +next
  1.1148 +  case Protected
  1.1149 +  with dyn_override wf
  1.1150 +  have "G \<turnstile> new overrides\<^sub>S old"
  1.1151 +    by (auto intro: dynamic_to_static_overriding)
  1.1152 +  with wf 
  1.1153 +  have "accmodi old \<le> accmodi new"
  1.1154 +    by (auto dest: wf_prog_stat_overridesD)
  1.1155 +  with Protected accmodi_new
  1.1156 +  show ?thesis
  1.1157 +    by (simp add: less_acc_def le_acc_def)
  1.1158 +next
  1.1159 +  case Public
  1.1160 +  with dyn_override wf
  1.1161 +  have "G \<turnstile> new overrides\<^sub>S old"
  1.1162 +    by (auto intro: dynamic_to_static_overriding)
  1.1163 +  with wf 
  1.1164 +  have "accmodi old \<le> accmodi new"
  1.1165 +    by (auto dest: wf_prog_stat_overridesD)
  1.1166 +  with Public accmodi_new
  1.1167 +  show ?thesis
  1.1168 +    by (simp add: less_acc_def le_acc_def)
  1.1169 +qed
  1.1170 +
  1.1171 +lemma dyn_override_Package:
  1.1172 + (assumes dyn_override: "G \<turnstile> new overrides old" and
  1.1173 +          accmodi_old: "accmodi old = Package" and 
  1.1174 +          accmodi_new: "accmodi new = Package" and
  1.1175 +                    wf: "wf_prog G"
  1.1176 + ) "pid (declclass old) = pid (declclass new)"
  1.1177 +proof - 
  1.1178 +  from dyn_override accmodi_old accmodi_new
  1.1179 +  show ?thesis (is "?EqPid old new")
  1.1180 +  proof (induct rule: overridesR.induct)
  1.1181 +    case (Direct new old)
  1.1182 +    assume "accmodi old = Package"
  1.1183 +           "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1.1184 +    then show "pid (declclass old) =  pid (declclass new)"
  1.1185 +      by (auto simp add: inheritable_in_def)
  1.1186 +  next
  1.1187 +    case (Indirect inter new old)
  1.1188 +    assume accmodi_old: "accmodi old = Package" and
  1.1189 +           accmodi_new: "accmodi new = Package" 
  1.1190 +    assume "G \<turnstile> new overrides inter"
  1.1191 +    with accmodi_new wf
  1.1192 +    have "accmodi inter = Package"
  1.1193 +      by  (auto intro: overrides_Package_old)
  1.1194 +    with Indirect
  1.1195 +    show "pid (declclass old) =  pid (declclass new)"
  1.1196 +      by auto
  1.1197 +  qed
  1.1198 +qed
  1.1199 +
  1.1200 +lemma dyn_override_Package_escape:
  1.1201 + (assumes dyn_override: "G \<turnstile> new overrides old" and
  1.1202 +          accmodi_old: "accmodi old = Package" and 
  1.1203 +         outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
  1.1204 +                    wf: "wf_prog G"
  1.1205 + ) "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
  1.1206 +             pid (declclass old) = pid (declclass inter) \<and>
  1.1207 +             Protected \<le> accmodi inter"
  1.1208 +proof -
  1.1209 +  from dyn_override accmodi_old outside_pack
  1.1210 +  show ?thesis (is "?P new old")
  1.1211 +  proof (induct rule: overridesR.induct)
  1.1212 +    case (Direct new old)
  1.1213 +    assume accmodi_old: "accmodi old = Package"
  1.1214 +    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1.1215 +    assume "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1.1216 +    with accmodi_old 
  1.1217 +    have "pid (declclass old) = pid (declclass new)"
  1.1218 +      by (simp add: inheritable_in_def)
  1.1219 +    with outside_pack 
  1.1220 +    show "?P new old"
  1.1221 +      by (contradiction)
  1.1222 +  next
  1.1223 +    case (Indirect inter new old)
  1.1224 +    assume accmodi_old: "accmodi old = Package"
  1.1225 +    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1.1226 +    assume override_new_inter: "G \<turnstile> new overrides inter"
  1.1227 +    assume override_inter_old: "G \<turnstile> inter overrides old"
  1.1228 +    assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 
  1.1229 +                           pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk>
  1.1230 +                           \<Longrightarrow> ?P new inter"
  1.1231 +    assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 
  1.1232 +                           pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk>
  1.1233 +                           \<Longrightarrow> ?P inter old"
  1.1234 +    show "?P new old"
  1.1235 +    proof (cases "pid (declclass old) = pid (declclass inter)")
  1.1236 +      case True
  1.1237 +      note same_pack_old_inter = this
  1.1238 +      show ?thesis
  1.1239 +      proof (cases "pid (declclass inter) = pid (declclass new)")
  1.1240 +	case True
  1.1241 +	with same_pack_old_inter outside_pack
  1.1242 +	show ?thesis
  1.1243 +	  by auto
  1.1244 +      next
  1.1245 +	case False
  1.1246 +	note diff_pack_inter_new = this
  1.1247 +	show ?thesis
  1.1248 +	proof (cases "accmodi inter = Package")
  1.1249 +	  case True
  1.1250 +	  with diff_pack_inter_new hyp_new_inter  
  1.1251 +	  obtain newinter where
  1.1252 +	    over_new_newinter: "G \<turnstile> new overrides newinter" and
  1.1253 +            over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
  1.1254 +            eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
  1.1255 +            accmodi_newinter: "Protected \<le> accmodi newinter"
  1.1256 +	    by auto
  1.1257 +	  from over_newinter_inter override_inter_old
  1.1258 +	  have "G\<turnstile>newinter overrides old"
  1.1259 +	    by (rule overridesR.Indirect)
  1.1260 +	  moreover
  1.1261 +	  from eq_pid same_pack_old_inter 
  1.1262 +	  have "pid (declclass old) = pid (declclass newinter)"
  1.1263 +	    by simp
  1.1264 +	  moreover
  1.1265 +	  note over_new_newinter accmodi_newinter
  1.1266 +	  ultimately show ?thesis
  1.1267 +	    by blast
  1.1268 +	next
  1.1269 +	  case False
  1.1270 +	  with override_new_inter
  1.1271 +	  have "Protected \<le> accmodi inter"
  1.1272 +	    by (cases "accmodi inter") (auto dest: no_Private_override)
  1.1273 +	  with override_new_inter override_inter_old same_pack_old_inter
  1.1274 +	  show ?thesis
  1.1275 +	    by blast
  1.1276 +	qed
  1.1277 +      qed
  1.1278 +    next
  1.1279 +      case False
  1.1280 +      with accmodi_old hyp_inter_old
  1.1281 +      obtain newinter where
  1.1282 +	over_inter_newinter: "G \<turnstile> inter overrides newinter" and
  1.1283 +          over_newinter_old: "G \<turnstile> newinter overrides old" and 
  1.1284 +                eq_pid: "pid (declclass old) = pid (declclass newinter)" and
  1.1285 +	accmodi_newinter: "Protected \<le> accmodi newinter"
  1.1286 +	by auto
  1.1287 +      from override_new_inter over_inter_newinter 
  1.1288 +      have "G \<turnstile> new overrides newinter"
  1.1289 +	by (rule overridesR.Indirect)
  1.1290 +      with eq_pid over_newinter_old accmodi_newinter
  1.1291 +      show ?thesis
  1.1292 +	by blast
  1.1293 +    qed
  1.1294 +  qed
  1.1295 +qed
  1.1296 +
  1.1297 +declare split_paired_All [simp del] split_paired_Ex [simp del]
  1.1298 +ML_setup {*
  1.1299 +simpset_ref() := simpset() delloop "split_all_tac";
  1.1300 +claset_ref () := claset () delSWrapper "split_all_tac"
  1.1301 +*}
  1.1302 +
  1.1303 +lemma declclass_widen[rule_format]: 
  1.1304 + "wf_prog G 
  1.1305 + \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1.1306 + \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1.1307 +proof (rule class_rec.induct,intro allI impI)
  1.1308 +  fix G C c m
  1.1309 +  assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
  1.1310 +               \<longrightarrow> ?P G (super c)"
  1.1311 +  assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  1.1312 +         m:  "methd G C sig = Some m"
  1.1313 +  show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
  1.1314 +  proof (cases "C=Object")
  1.1315 +    case True 
  1.1316 +    with wf m show ?thesis by (simp add: methd_Object_SomeD)
  1.1317 +  next
  1.1318 +    let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  1.1319 +    let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1.1320 +    case False 
  1.1321 +    with cls_C wf m
  1.1322 +    have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  1.1323 +      by (simp add: methd_rec)
  1.1324 +    show ?thesis
  1.1325 +    proof (cases "?table sig")
  1.1326 +      case None
  1.1327 +      from this methd_C have "?filter (methd G (super c)) sig = Some m"
  1.1328 +	by simp
  1.1329 +      moreover
  1.1330 +      from wf cls_C False obtain sup where "class G (super c) = Some sup"
  1.1331 +	by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1.1332 +      moreover note wf False cls_C Hyp 
  1.1333 +      ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  by auto
  1.1334 +      moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I)
  1.1335 +      ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
  1.1336 +    next
  1.1337 +      case Some
  1.1338 +      from this wf False cls_C methd_C show ?thesis by auto
  1.1339 +    qed
  1.1340 +  qed
  1.1341 +qed
  1.1342 +
  1.1343 +(*
  1.1344 +lemma declclass_widen[rule_format]: 
  1.1345 + "wf_prog G 
  1.1346 + \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1.1347 + \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1.1348 +apply (rule class_rec.induct)
  1.1349 +apply (rule impI)+
  1.1350 +apply (case_tac "C=Object")
  1.1351 +apply   (force simp add: methd_Object_SomeD)
  1.1352 +
  1.1353 +apply   (rule allI)+
  1.1354 +apply   (rule impI)
  1.1355 +apply   (simp (no_asm_simp) add: methd_rec)
  1.1356 +apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
  1.1357 +apply    (simp add: override_def)
  1.1358 +apply    (frule (1) subcls1I)
  1.1359 +apply    (drule (1) wf_prog_cdecl)
  1.1360 +apply    (drule (1) wf_cdecl_supD)
  1.1361 +apply    clarify
  1.1362 +apply    (drule is_acc_class_is_class)
  1.1363 +apply    clarify
  1.1364 +apply    (blast dest: rtrancl_into_rtrancl2)
  1.1365 +
  1.1366 +apply    auto
  1.1367 +done
  1.1368 +*)
  1.1369 +
  1.1370 +(*
  1.1371 +lemma accessible_public_inheritance_lemma1:
  1.1372 +  "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object; accmodi m = Public;
  1.1373 +    G\<turnstile>m accessible_through_inheritance_in (super c)\<rbrakk> 
  1.1374 +   \<Longrightarrow> G\<turnstile>m accessible_through_inheritance_in C"
  1.1375 +apply   (frule (1) subcls1I)
  1.1376 +apply   (rule accessible_through_inheritance.Indirect)
  1.1377 +apply     (blast)
  1.1378 +apply     (erule accessible_through_inheritance_subclsD)
  1.1379 +apply     (blast dest: wf_prog_acc_superD is_acc_classD)
  1.1380 +apply     assumption
  1.1381 +apply     (force dest: wf_prog_acc_superD is_acc_classD
  1.1382 +                 simp add: accessible_for_inheritance_in_def)
  1.1383 +done
  1.1384 +
  1.1385 +lemma accessible_public_inheritance_lemma[rule_format]:
  1.1386 +  "\<lbrakk>wf_prog G;C \<noteq> Object; class G C = Some c; 
  1.1387 +    accmodi m = Public
  1.1388 +   \<rbrakk> \<Longrightarrow> methd G (super c) sig = Some m 
  1.1389 +        \<longrightarrow> G\<turnstile>m accessible_through_inheritance_in C" 
  1.1390 +apply (frule (2) wf_prog_acc_superD [THEN is_acc_classD])
  1.1391 +apply (erule conjE)
  1.1392 +apply (simp only: not_None_eq)
  1.1393 +apply (erule exE)
  1.1394 +apply (case_tac "(super c) = Object")
  1.1395 +apply   (rule impI)
  1.1396 +apply   (rule accessible_through_inheritance.Direct)
  1.1397 +apply     force
  1.1398 +apply     (force simp add: accessible_for_inheritance_in_def)
  1.1399 +
  1.1400 +apply   (frule wf_ws_prog) 
  1.1401 +apply   (simp add: methd_rec)
  1.1402 +apply   (case_tac "table_of (map (\<lambda>(s, m). (s, super c, m)) (methods y)) sig")
  1.1403 +apply     simp
  1.1404 +apply     (clarify)
  1.1405 +apply     (rule_tac D="super c" in accessible_through_inheritance.Indirect)
  1.1406 +apply       (blast dest: subcls1I)
  1.1407 +apply       (blast)
  1.1408 +apply       simp
  1.1409 +apply       assumption
  1.1410 +apply       (simp add: accessible_for_inheritance_in_def)
  1.1411 +
  1.1412 +apply     clarsimp
  1.1413 +apply     (rule accessible_through_inheritance.Direct)
  1.1414 +apply     (auto dest: subcls1I simp add: accessible_for_inheritance_in_def)
  1.1415 +done
  1.1416 +
  1.1417 +lemma accessible_public_inheritance:
  1.1418 +  "\<lbrakk>wf_prog G; class G D = Some d; G\<turnstile>C \<prec>\<^sub>C D; methd G D sig = Some m; 
  1.1419 +    accmodi m = Public\<rbrakk> 
  1.1420 +   \<Longrightarrow> G \<turnstile> m accessible_through_inheritance_in C"
  1.1421 +apply (erule converse_trancl_induct)
  1.1422 +apply  (blast dest: subcls1D intro: accessible_public_inheritance_lemma)
  1.1423 +
  1.1424 +apply  (frule subcls1D)
  1.1425 +apply  clarify
  1.1426 +apply  (frule  (2) wf_prog_acc_superD [THEN is_acc_classD])
  1.1427 +apply  clarify
  1.1428 +apply  (rule_tac D="super c" in accessible_through_inheritance.Indirect)
  1.1429 +apply   (auto intro:trancl_into_trancl2 
  1.1430 +                    accessible_through_inheritance_subclsD
  1.1431 +              simp add: accessible_for_inheritance_in_def)
  1.1432 +done
  1.1433 +*)
  1.1434 +
  1.1435 +
  1.1436 +lemma declclass_methd_Object: 
  1.1437 + "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object"
  1.1438 +by auto
  1.1439 +
  1.1440 +
  1.1441 +lemma methd_declaredD: 
  1.1442 + "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 
  1.1443 +  \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1.1444 +proof -
  1.1445 +  assume    wf: "wf_prog G"
  1.1446 +  then have ws: "ws_prog G" ..
  1.1447 +  assume  clsC: "is_class G C"
  1.1448 +  from clsC ws 
  1.1449 +  show "methd G C sig = Some m 
  1.1450 +        \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1.1451 +    (is "PROP ?P C") 
  1.1452 +  proof (induct ?P C rule: ws_class_induct')
  1.1453 +    case Object
  1.1454 +    assume "methd G Object sig = Some m" 
  1.1455 +    with wf show ?thesis
  1.1456 +      by - (rule method_declared_inI, auto) 
  1.1457 +  next
  1.1458 +    case Subcls
  1.1459 +    fix C c
  1.1460 +    assume clsC: "class G C = Some c"
  1.1461 +    and       m: "methd G C sig = Some m"
  1.1462 +    and     hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 
  1.1463 +    let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1.1464 +    show ?thesis
  1.1465 +    proof (cases "?newMethods sig")
  1.1466 +      case None
  1.1467 +      from None ws clsC m hyp 
  1.1468 +      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
  1.1469 +    next
  1.1470 +      case Some
  1.1471 +      from Some ws clsC m 
  1.1472 +      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
  1.1473 +    qed
  1.1474 +  qed
  1.1475 +qed
  1.1476 +
  1.1477 +
  1.1478 +lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
  1.1479 +(assumes methd_C: "methd G C sig = Some m" and
  1.1480 +                    ws: "ws_prog G" and
  1.1481 +                  clsC: "class G C = Some c" and
  1.1482 +             neq_C_Obj: "C\<noteq>Object" )  
  1.1483 +"\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
  1.1484 +  \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
  1.1485 + \<rbrakk> \<Longrightarrow> P"
  1.1486 +proof -
  1.1487 +  let ?inherited   = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 
  1.1488 +                              (methd G (super c))"
  1.1489 +  let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1.1490 +  from ws clsC neq_C_Obj methd_C 
  1.1491 +  have methd_unfold: "(?inherited ++ ?new) sig = Some m"
  1.1492 +    by (simp add: methd_rec)
  1.1493 +  assume NewMethod: "?new sig = Some m \<Longrightarrow> P"
  1.1494 +  assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); 
  1.1495 +                            methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P"
  1.1496 +  show P
  1.1497 +  proof (cases "?new sig")
  1.1498 +    case None
  1.1499 +    with methd_unfold have "?inherited sig = Some m"
  1.1500 +      by (auto)
  1.1501 +    with InheritedMethod show P by blast
  1.1502 +  next
  1.1503 +    case Some
  1.1504 +    with methd_unfold have "?new sig = Some m"
  1.1505 +      by auto
  1.1506 +    with NewMethod show P by blast
  1.1507 +  qed
  1.1508 +qed
  1.1509 +
  1.1510 +  
  1.1511 +lemma methd_member_of:
  1.1512 + (assumes wf: "wf_prog G") 
  1.1513 +  "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
  1.1514 +  (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
  1.1515 +proof -
  1.1516 +  from wf   have   ws: "ws_prog G" ..
  1.1517 +  assume defC: "is_class G C"
  1.1518 +  from defC ws 
  1.1519 +  show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
  1.1520 +  proof (induct rule: ws_class_induct')  
  1.1521 +    case Object
  1.1522 +    with wf have declC: "declclass m = Object"
  1.1523 +      by (blast intro: declclass_methd_Object)
  1.1524 +    with Object wf have "G\<turnstile>Methd sig m declared_in Object"
  1.1525 +      by (auto dest: methd_declaredD simp del: methd_Object)
  1.1526 +    with declC 
  1.1527 +    show "?MemberOf Object"
  1.1528 +      by (auto intro!: members.Immediate
  1.1529 +                  simp del: methd_Object)
  1.1530 +  next
  1.1531 +    case (Subcls C c)
  1.1532 +    assume  clsC: "class G C = Some c" and
  1.1533 +       neq_C_Obj: "C \<noteq> Object"  
  1.1534 +    assume methd: "?Method C"
  1.1535 +    from methd ws clsC neq_C_Obj
  1.1536 +    show "?MemberOf C"
  1.1537 +    proof (cases rule: methd_rec_Some_cases)
  1.1538 +      case NewMethod
  1.1539 +      with clsC show ?thesis
  1.1540 +	by (auto dest: method_declared_inI intro!: members.Immediate)
  1.1541 +    next
  1.1542 +      case InheritedMethod
  1.1543 +      then show "?thesis"
  1.1544 +	by (blast dest: inherits_member)
  1.1545 +    qed
  1.1546 +  qed
  1.1547 +qed
  1.1548 +
  1.1549 +lemma current_methd: 
  1.1550 +      "\<lbrakk>table_of (methods c) sig = Some new;
  1.1551 +        ws_prog G; class G C = Some c; C \<noteq> Object; 
  1.1552 +        methd G (super c) sig = Some old\<rbrakk> 
  1.1553 +    \<Longrightarrow> methd G C sig = Some (C,new)"
  1.1554 +by (auto simp add: methd_rec
  1.1555 +            intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
  1.1556 +
  1.1557 +lemma wf_prog_staticD:
  1.1558 + (assumes     wf: "wf_prog G" and 
  1.1559 +            clsC: "class G C = Some c" and
  1.1560 +       neq_C_Obj: "C \<noteq> Object" and 
  1.1561 +             old: "methd G (super c) sig = Some old" and 
  1.1562 +     accmodi_old: "Protected \<le> accmodi old" and
  1.1563 +             new: "table_of (methods c) sig = Some new"
  1.1564 + ) "is_static new = is_static old"
  1.1565 +proof -
  1.1566 +  from clsC wf 
  1.1567 +  have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
  1.1568 +  from wf clsC neq_C_Obj
  1.1569 +  have is_cls_super: "is_class G (super c)" 
  1.1570 +    by (blast dest: wf_prog_acc_superD is_acc_classD)
  1.1571 +  from wf is_cls_super old 
  1.1572 +  have old_member_of: "G\<turnstile>Methd sig old member_of (super c)"  
  1.1573 +    by (rule methd_member_of)
  1.1574 +  from old wf is_cls_super 
  1.1575 +  have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)"
  1.1576 +    by (auto dest: methd_declared_in_declclass)
  1.1577 +  from new clsC 
  1.1578 +  have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C"
  1.1579 +    by (auto intro: method_declared_inI)
  1.1580 +  note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
  1.1581 +  from clsC neq_C_Obj
  1.1582 +  have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1.1583 +    by (rule subcls1I)
  1.1584 +  then have "G\<turnstile>C \<prec>\<^sub>C super c" ..
  1.1585 +  also from old wf is_cls_super
  1.1586 +  have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC)
  1.1587 +  finally have subcls_C_old:  "G\<turnstile>C \<prec>\<^sub>C (declclass old)" .
  1.1588 +  from accmodi_old 
  1.1589 +  have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C"
  1.1590 +    by (auto simp add: inheritable_in_def
  1.1591 +                 dest: acc_modi_le_Dests)
  1.1592 +  show ?thesis
  1.1593 +  proof (cases "is_static new")
  1.1594 +    case True
  1.1595 +    with subcls_C_old new_declared old_declared inheritable
  1.1596 +    have "G,sig\<turnstile>(C,new) hides old"
  1.1597 +      by (auto intro: hidesI)
  1.1598 +    with True wf_cdecl neq_C_Obj new 
  1.1599 +    show ?thesis
  1.1600 +      by (auto dest: wf_cdecl_hides_SomeD)
  1.1601 +  next
  1.1602 +    case False
  1.1603 +    with subcls_C_old new_declared old_declared inheritable subcls1_C_super
  1.1604 +         old_member_of
  1.1605 +    have "G,sig\<turnstile>(C,new) overrides\<^sub>S old"
  1.1606 +      by (auto intro: stat_overridesR.Direct)
  1.1607 +    with False wf_cdecl neq_C_Obj new 
  1.1608 +    show ?thesis
  1.1609 +      by (auto dest: wf_cdecl_overrides_SomeD)
  1.1610 +  qed
  1.1611 +qed
  1.1612 +
  1.1613 +lemma inheritable_instance_methd: 
  1.1614 + (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1.1615 +              is_cls_D: "is_class G D" and
  1.1616 +                    wf: "wf_prog G" and 
  1.1617 +                   old: "methd G D sig = Some old" and
  1.1618 +           accmodi_old: "Protected \<le> accmodi old" and  
  1.1619 +        not_static_old: "\<not> is_static old"
  1.1620 + )  
  1.1621 +  "\<exists>new. methd G C sig = Some new \<and>
  1.1622 +         (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
  1.1623 + (is "(\<exists>new. (?Constraint C new old))")
  1.1624 +proof -
  1.1625 +  from subclseq_C_D is_cls_D 
  1.1626 +  have is_cls_C: "is_class G C" by (rule subcls_is_class2) 
  1.1627 +  from wf 
  1.1628 +  have ws: "ws_prog G" ..
  1.1629 +  from is_cls_C ws subclseq_C_D 
  1.1630 +  show "\<exists>new. ?Constraint C new old"
  1.1631 +  proof (induct rule: ws_class_induct')
  1.1632 +    case (Object co)
  1.1633 +    then have eq_D_Obj: "D=Object" by auto
  1.1634 +    with old 
  1.1635 +    have "?Constraint Object old old"
  1.1636 +      by auto
  1.1637 +    with eq_D_Obj 
  1.1638 +    show "\<exists> new. ?Constraint Object new old" by auto
  1.1639 +  next
  1.1640 +    case (Subcls C c)
  1.1641 +    assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old"
  1.1642 +    assume clsC: "class G C = Some c"
  1.1643 +    assume neq_C_Obj: "C\<noteq>Object"
  1.1644 +    from clsC wf 
  1.1645 +    have wf_cdecl: "wf_cdecl G (C,c)" 
  1.1646 +      by (rule wf_prog_cdecl)
  1.1647 +    from ws clsC neq_C_Obj
  1.1648 +    have is_cls_super: "is_class G (super c)"
  1.1649 +      by (auto dest: ws_prog_cdeclD)
  1.1650 +    from clsC wf neq_C_Obj 
  1.1651 +    have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and
  1.1652 +	 subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1.1653 +      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
  1.1654 +              intro: subcls1I)
  1.1655 +    show "\<exists>new. ?Constraint C new old"
  1.1656 +    proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D")
  1.1657 +      case False
  1.1658 +      from False Subcls 
  1.1659 +      have eq_C_D: "C=D"
  1.1660 +	by (auto dest: subclseq_superD)
  1.1661 +      with old 
  1.1662 +      have "?Constraint C old old"
  1.1663 +	by auto
  1.1664 +      with eq_C_D 
  1.1665 +      show "\<exists> new. ?Constraint C new old" by auto
  1.1666 +    next
  1.1667 +      case True
  1.1668 +      with hyp obtain super_method
  1.1669 +	where super: "?Constraint (super c) super_method old" by blast
  1.1670 +      from super not_static_old
  1.1671 +      have not_static_super: "\<not> is_static super_method"
  1.1672 +	by (auto dest!: stat_overrides_commonD)
  1.1673 +      from super old wf accmodi_old
  1.1674 +      have accmodi_super_method: "Protected \<le> accmodi super_method"
  1.1675 +	by (auto dest!: wf_prog_stat_overridesD
  1.1676 +                 intro: order_trans)
  1.1677 +      from super accmodi_old wf
  1.1678 +      have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
  1.1679 +	by (auto dest!: wf_prog_stat_overridesD
  1.1680 +                        acc_modi_le_Dests
  1.1681 +              simp add: inheritable_in_def)	           
  1.1682 +      from super wf is_cls_super
  1.1683 +      have member: "G\<turnstile>Methd sig super_method member_of (super c)"
  1.1684 +	by (auto intro: methd_member_of) 
  1.1685 +      from member
  1.1686 +      have decl_super_method:
  1.1687 +        "G\<turnstile>Methd sig super_method declared_in (declclass super_method)"
  1.1688 +	by (auto dest: member_of_declC)
  1.1689 +      from super subcls1_C_super ws is_cls_super 
  1.1690 +      have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)"
  1.1691 +	by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 
  1.1692 +      show "\<exists> new. ?Constraint C new old"
  1.1693 +      proof (cases "methd G C sig")
  1.1694 +	case None
  1.1695 +	have "methd G (super c) sig = None"
  1.1696 +	proof -
  1.1697 +	  from clsC ws None 
  1.1698 +	  have no_new: "table_of (methods c) sig = None" 
  1.1699 +	    by (auto simp add: methd_rec)
  1.1700 +	  with clsC 
  1.1701 +	  have undeclared: "G\<turnstile>mid sig undeclared_in C"
  1.1702 +	    by (auto simp add: undeclared_in_def cdeclaredmethd_def)
  1.1703 +	  with inheritable member superAccessible subcls1_C_super
  1.1704 +	  have inherits: "G\<turnstile>C inherits (method sig super_method)"
  1.1705 +	    by (auto simp add: inherits_def)
  1.1706 +	  with clsC ws no_new super neq_C_Obj
  1.1707 +	  have "methd G C sig = Some super_method"
  1.1708 +	    by (auto simp add: methd_rec override_def
  1.1709 +	                intro: filter_tab_SomeI)
  1.1710 +          with None show ?thesis
  1.1711 +	    by simp
  1.1712 +	qed
  1.1713 +	with super show ?thesis by auto
  1.1714 +      next
  1.1715 +	case (Some new)
  1.1716 +	from this ws clsC neq_C_Obj
  1.1717 +	show ?thesis
  1.1718 +	proof (cases rule: methd_rec_Some_cases)
  1.1719 +	  case InheritedMethod
  1.1720 +	  with super Some show ?thesis 
  1.1721 +	    by auto
  1.1722 +	next
  1.1723 +	  case NewMethod
  1.1724 +	  assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig 
  1.1725 +                       = Some new"
  1.1726 +	  from new 
  1.1727 +	  have declcls_new: "declclass new = C" 
  1.1728 +	    by auto
  1.1729 +	  from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
  1.1730 +	  have not_static_new: "\<not> is_static new" 
  1.1731 +	    by (auto dest: wf_prog_staticD) 
  1.1732 +	  from clsC new
  1.1733 +	  have decl_new: "G\<turnstile>Methd sig new declared_in C"
  1.1734 +	    by (auto simp add: declared_in_def cdeclaredmethd_def)
  1.1735 +	  from not_static_new decl_new decl_super_method
  1.1736 +	       member subcls1_C_super inheritable declcls_new subcls_C_super 
  1.1737 +	  have "G,sig\<turnstile> new overrides\<^sub>S super_method"
  1.1738 +	    by (auto intro: stat_overridesR.Direct) 
  1.1739 +	  with super Some
  1.1740 +	  show ?thesis
  1.1741 +	    by (auto intro: stat_overridesR.Indirect)
  1.1742 +	qed
  1.1743 +      qed
  1.1744 +    qed
  1.1745 +  qed
  1.1746 +qed
  1.1747 +
  1.1748 +lemma inheritable_instance_methd_cases [consumes 6
  1.1749 +                                       , case_names Inheritance Overriding]: 
  1.1750 + (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1.1751 +              is_cls_D: "is_class G D" and
  1.1752 +                    wf: "wf_prog G" and 
  1.1753 +                   old: "methd G D sig = Some old" and
  1.1754 +           accmodi_old: "Protected \<le> accmodi old" and  
  1.1755 +        not_static_old: "\<not> is_static old" and
  1.1756 +           inheritance:  "methd G C sig = Some old \<Longrightarrow> P" and
  1.1757 +            overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
  1.1758 +                                   G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
  1.1759 +        
  1.1760 + ) "P"
  1.1761 +proof -
  1.1762 +from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1.1763 +     inheritance overriding
  1.1764 +show ?thesis
  1.1765 +  by (auto dest: inheritable_instance_methd)
  1.1766 +qed
  1.1767 +
  1.1768 +lemma inheritable_instance_methd_props: 
  1.1769 + (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1.1770 +              is_cls_D: "is_class G D" and
  1.1771 +                    wf: "wf_prog G" and 
  1.1772 +                   old: "methd G D sig = Some old" and
  1.1773 +           accmodi_old: "Protected \<le> accmodi old" and  
  1.1774 +        not_static_old: "\<not> is_static old"
  1.1775 + )  
  1.1776 +  "\<exists>new. methd G C sig = Some new \<and>
  1.1777 +          \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
  1.1778 + (is "(\<exists>new. (?Constraint C new old))")
  1.1779 +proof -
  1.1780 +  from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1.1781 +  show ?thesis
  1.1782 +  proof (cases rule: inheritable_instance_methd_cases)
  1.1783 +    case Inheritance
  1.1784 +    with not_static_old accmodi_old show ?thesis by auto
  1.1785 +  next
  1.1786 +    case (Overriding new)
  1.1787 +    then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
  1.1788 +    with Overriding not_static_old accmodi_old wf 
  1.1789 +    show ?thesis 
  1.1790 +      by (auto dest!: wf_prog_stat_overridesD
  1.1791 +               intro: order_trans)
  1.1792 +  qed
  1.1793 +qed
  1.1794 + 	  
  1.1795 +(* ### Probleme: Die tollen methd_subcls_cases Lemma wird warscheinlich
  1.1796 +  kaum gebraucht: 
  1.1797 +Redundanz: stat_overrides.Direct old declared in declclass old folgt aus
  1.1798 +           member of 
  1.1799 +   Problem: Predikate wie overrides, sind global üper die Hierarchie hinweg
  1.1800 +            definiert, aber oft barucht man eben zusätlich Induktion
  1.1801 +            : von super c auf C; Dann ist aber auss dem Kontext
  1.1802 +            die Unterscheidung in die 5 fälle overkill,
  1.1803 +            da man dann warscheinlich meistens eh in einem speziellen
  1.1804 +            Fall kommt (durch die Hypothesen)
  1.1805 +*)
  1.1806 +    
  1.1807 +(* local lemma *)
  1.1808 +ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
  1.1809 +ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
  1.1810 +lemma subint_widen_imethds: 
  1.1811 + "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
  1.1812 +  \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
  1.1813 +                          accmodi im = accmodi jm \<and>
  1.1814 +                          G\<turnstile>resTy im\<preceq>resTy jm"
  1.1815 +proof -
  1.1816 +  assume irel: "G\<turnstile>I\<preceq>I J" and
  1.1817 +           wf: "wf_prog G" and
  1.1818 +     is_iface: "is_iface G J"
  1.1819 +  from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
  1.1820 +               (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
  1.1821 +  proof (induct ?P I rule: converse_rtrancl_induct) 
  1.1822 +    case Id
  1.1823 +    assume "jm \<in> imethds G J sig"
  1.1824 +    then show "?Concl J" by  (blast elim: bexI')
  1.1825 +  next
  1.1826 +    case Step
  1.1827 +    fix I SI
  1.1828 +    assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
  1.1829 +            subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
  1.1830 +                    hyp: "PROP ?P SI" and
  1.1831 +                     jm: "jm \<in> imethds G J sig"
  1.1832 +    from subint1_I_SI 
  1.1833 +    obtain i where
  1.1834 +      ifI: "iface G I = Some i" and
  1.1835 +       SI: "SI \<in> set (isuperIfs i)"
  1.1836 +      by (blast dest: subint1D)
  1.1837 +
  1.1838 +    let ?newMethods 
  1.1839 +          = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
  1.1840 +    show "?Concl I"
  1.1841 +    proof (cases "?newMethods sig = {}")
  1.1842 +      case True
  1.1843 +      with ifI SI hyp wf jm 
  1.1844 +      show "?thesis" 
  1.1845 +	by (auto simp add: imethds_rec) 
  1.1846 +    next
  1.1847 +      case False
  1.1848 +      from ifI wf False
  1.1849 +      have imethds: "imethds G I sig = ?newMethods sig"
  1.1850 +	by (simp add: imethds_rec)
  1.1851 +      from False
  1.1852 +      obtain im where
  1.1853 +        imdef: "im \<in> ?newMethods sig" 
  1.1854 +	by (blast)
  1.1855 +      with imethds 
  1.1856 +      have im: "im \<in> imethds G I sig"
  1.1857 +	by (blast)
  1.1858 +      with im wf ifI 
  1.1859 +      obtain
  1.1860 +	 imStatic: "\<not> is_static im" and
  1.1861 +         imPublic: "accmodi im = Public"
  1.1862 +	by (auto dest!: imethds_wf_mhead)	
  1.1863 +      from ifI wf 
  1.1864 +      have wf_I: "wf_idecl G (I,i)" 
  1.1865 +	by (rule wf_prog_idecl)
  1.1866 +      with SI wf  
  1.1867 +      obtain si where
  1.1868 +	 ifSI: "iface G SI = Some si" and
  1.1869 +	wf_SI: "wf_idecl G (SI,si)" 
  1.1870 +	by (auto dest!: wf_idecl_supD is_acc_ifaceD
  1.1871 +                  dest: wf_prog_idecl)
  1.1872 +      from jm hyp 
  1.1873 +      obtain sim::"qtname \<times> mhead"  where
  1.1874 +                      sim: "sim \<in> imethds G SI sig" and
  1.1875 +         eq_static_sim_jm: "is_static sim = is_static jm" and 
  1.1876 +         eq_access_sim_jm: "accmodi sim = accmodi jm" and 
  1.1877 +        resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm"
  1.1878 +	by blast
  1.1879 +      with wf_I SI imdef sim 
  1.1880 +      have "G\<turnstile>resTy im\<preceq>resTy sim"   
  1.1881 +	by (auto dest!: wf_idecl_hidings hidings_entailsD)
  1.1882 +      with wf resTy_widen_sim_jm 
  1.1883 +      have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm"
  1.1884 +	by (blast intro: widen_trans)
  1.1885 +      from sim wf ifSI  
  1.1886 +      obtain
  1.1887 +	simStatic: "\<not> is_static sim" and
  1.1888 +        simPublic: "accmodi sim = Public"
  1.1889 +	by (auto dest!: imethds_wf_mhead)
  1.1890 +      from im 
  1.1891 +           imStatic simStatic eq_static_sim_jm
  1.1892 +           imPublic simPublic eq_access_sim_jm
  1.1893 +           resTy_widen_im_jm
  1.1894 +      show ?thesis 
  1.1895 +	by auto 
  1.1896 +    qed
  1.1897 +  qed
  1.1898 +qed
  1.1899 +     
  1.1900 +(* Tactical version *)
  1.1901 +(* 
  1.1902 +lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow>  
  1.1903 +  \<forall> jm \<in> imethds G J sig.  
  1.1904 +  \<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> 
  1.1905 +                          access (mthd im)= access (mthd jm) \<and>
  1.1906 +                          G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)"
  1.1907 +apply (erule converse_rtrancl_induct)
  1.1908 +apply  (clarsimp elim!: bexI')
  1.1909 +apply (frule subint1D)
  1.1910 +apply clarify
  1.1911 +apply (erule ballE')
  1.1912 +apply  fast
  1.1913 +apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl)
  1.1914 +apply clarsimp
  1.1915 +apply (subst imethds_rec, assumption, erule wf_ws_prog)
  1.1916 +apply (unfold overrides_t_def)
  1.1917 +apply (drule (1) wf_prog_idecl)
  1.1918 +apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
  1.1919 +                                       [THEN is_acc_ifaceD [THEN conjunct1]]]])
  1.1920 +apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
  1.1921 +                  sig ={}")
  1.1922 +apply   force
  1.1923 +
  1.1924 +apply   (simp only:)
  1.1925 +apply   (simp)
  1.1926 +apply   clarify
  1.1927 +apply   (frule wf_idecl_hidings [THEN hidings_entailsD])
  1.1928 +apply     blast
  1.1929 +apply     blast
  1.1930 +apply   (rule bexI')
  1.1931 +apply     simp
  1.1932 +apply     (drule table_of_map_SomeI [of _ "sig"])
  1.1933 +apply     simp
  1.1934 +
  1.1935 +apply     (frule wf_idecl_mhead [of _ _ _ "sig"])
  1.1936 +apply       (rule table_of_Some_in_set)
  1.1937 +apply       assumption
  1.1938 +apply     auto
  1.1939 +done
  1.1940 +*)
  1.1941 +    
  1.1942 +
  1.1943 +(* local lemma *)
  1.1944 +lemma implmt1_methd: 
  1.1945 + "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow>  
  1.1946 +  \<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> 
  1.1947 +                       G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1.1948 +                       accmodi im = Public \<and> accmodi cm = Public"
  1.1949 +apply (drule implmt1D)
  1.1950 +apply clarify
  1.1951 +apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
  1.1952 +apply (frule (1) imethds_wf_mhead)
  1.1953 +apply  (simp add: is_acc_iface_def)
  1.1954 +apply (force)
  1.1955 +done
  1.1956 +
  1.1957 +
  1.1958 +(* local lemma *)
  1.1959 +lemma implmt_methd [rule_format (no_asm)]: 
  1.1960 +"\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow>  
  1.1961 + (\<forall> im    \<in>imethds G I   sig.  
  1.1962 +  \<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> 
  1.1963 +                      G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1.1964 +                      accmodi im = Public \<and> accmodi cm = Public)"
  1.1965 +apply (frule implmt_is_class)
  1.1966 +apply (erule implmt.induct)
  1.1967 +apply   safe
  1.1968 +apply   (drule (2) implmt1_methd)
  1.1969 +apply   fast
  1.1970 +apply  (drule (1) subint_widen_imethds)
  1.1971 +apply   simp
  1.1972 +apply   assumption
  1.1973 +apply  clarify
  1.1974 +apply  (drule (2) implmt1_methd)
  1.1975 +apply  (force)
  1.1976 +apply (frule subcls1D)
  1.1977 +apply (drule (1) bspec)
  1.1978 +apply clarify
  1.1979 +apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 
  1.1980 +                                 OF _ implmt_is_class])
  1.1981 +apply auto 
  1.1982 +done
  1.1983 +
  1.1984 +
  1.1985 +declare split_paired_All [simp] split_paired_Ex [simp]
  1.1986 +ML_setup {*
  1.1987 +claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  1.1988 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  1.1989 +*}
  1.1990 +lemma mheadsD [rule_format (no_asm)]: 
  1.1991 +"emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow>
  1.1992 + (\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> 
  1.1993 +          accmethd G S C sig = Some m \<and>
  1.1994 +          (declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or>
  1.1995 + (\<exists>I. t = IfaceT I \<and> ((\<exists>im. im  \<in> accimethds G (pid S) I sig \<and> 
  1.1996 +          mthd im = mhd emh) \<or> 
  1.1997 +  (\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> 
  1.1998 +       accmodi m \<noteq> Private \<and> 
  1.1999 +       declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or>
  1.2000 + (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
  1.2001 +        accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 
  1.2002 +        declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
  1.2003 +apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1])
  1.2004 +apply auto
  1.2005 +apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
  1.2006 +apply (auto  dest!: accmethd_SomeD)
  1.2007 +done
  1.2008 +
  1.2009 +lemma mheads_cases [consumes 2, case_names Class_methd 
  1.2010 +                    Iface_methd Iface_Object_methd Array_Object_methd]: 
  1.2011 +"\<lbrakk>emh \<in> mheads G S t sig; wf_prog G;
  1.2012 + \<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m;
  1.2013 +           (declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh; 
  1.2014 + \<And> I im. \<lbrakk>t = IfaceT I; im  \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk>
  1.2015 +          \<Longrightarrow> P emh;
  1.2016 + \<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S);
  1.2017 +          accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
  1.2018 +         declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh;
  1.2019 + \<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S);
  1.2020 +          accmethd G S Object sig = Some m; accmodi m \<noteq> Private; 
  1.2021 +          declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow>  P emh 
  1.2022 +\<rbrakk> \<Longrightarrow> P emh"
  1.2023 +by (blast dest!: mheadsD)
  1.2024 +
  1.2025 +lemma declclassD[rule_format]:
  1.2026 + "\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; 
  1.2027 +   class G (declclass m) = Some d\<rbrakk>
  1.2028 +  \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)"
  1.2029 +proof -
  1.2030 +  assume    wf: "wf_prog G"
  1.2031 +  then have ws: "ws_prog G" ..
  1.2032 +  assume  clsC: "class G C = Some c"
  1.2033 +  from clsC ws 
  1.2034 +  show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
  1.2035 +        \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
  1.2036 +         (is "PROP ?P C") 
  1.2037 +  proof (induct ?P C rule: ws_class_induct)
  1.2038 +    case Object
  1.2039 +    fix m d
  1.2040 +    assume "methd G Object sig = Some m" 
  1.2041 +           "class G (declclass m) = Some d"
  1.2042 +    with wf show "?thesis m d" by auto
  1.2043 +  next
  1.2044 +    case Subcls
  1.2045 +    fix C c m d
  1.2046 +    assume hyp: "PROP ?P (super c)"
  1.2047 +    and      m: "methd G C sig = Some m"
  1.2048 +    and  declC: "class G (declclass m) = Some d"
  1.2049 +    and   clsC: "class G C = Some c"
  1.2050 +    and   nObj: "C \<noteq> Object"
  1.2051 +    let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
  1.2052 +    show "?thesis m d" 
  1.2053 +    proof (cases "?newMethods")
  1.2054 +      case None
  1.2055 +      from None clsC nObj ws m declC hyp  
  1.2056 +      show "?thesis" by (auto simp add: methd_rec)
  1.2057 +    next
  1.2058 +      case Some
  1.2059 +      from Some clsC nObj ws m declC hyp  
  1.2060 +      show "?thesis" 
  1.2061 +	by (auto simp add: methd_rec
  1.2062 +                     dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1.2063 +    qed
  1.2064 +  qed
  1.2065 +qed
  1.2066 +
  1.2067 +(* Tactical version *)
  1.2068 +(*
  1.2069 +lemma declclassD[rule_format]:
  1.2070 + "wf_prog G \<longrightarrow>  
  1.2071 + (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
  1.2072 +  class G (declclass m) = Some d
  1.2073 + \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
  1.2074 +apply (rule class_rec.induct)
  1.2075 +apply (rule impI)
  1.2076 +apply (rule allI)+
  1.2077 +apply (rule impI)
  1.2078 +apply (case_tac "C=Object")
  1.2079 +apply   (force simp add: methd_rec)
  1.2080 +
  1.2081 +apply   (subst methd_rec)
  1.2082 +apply     (blast dest: wf_ws_prog)+
  1.2083 +apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
  1.2084 +apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1.2085 +done
  1.2086 +*)
  1.2087 +
  1.2088 +lemma dynmethd_Object:
  1.2089 + (assumes statM: "methd G Object sig = Some statM" and
  1.2090 +        private: "accmodi statM = Private" and 
  1.2091 +       is_cls_C: "is_class G C" and
  1.2092 +             wf: "wf_prog G"
  1.2093 + ) "dynmethd G Object C sig = Some statM"
  1.2094 +proof -
  1.2095 +  from is_cls_C wf 
  1.2096 +  have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
  1.2097 +    by (auto intro: subcls_ObjectI)
  1.2098 +  from wf have ws: "ws_prog G" 
  1.2099 +    by simp
  1.2100 +  from wf 
  1.2101 +  have is_cls_Obj: "is_class G Object" 
  1.2102 +    by simp
  1.2103 +  from statM subclseq is_cls_Obj ws private
  1.2104 +  show ?thesis
  1.2105 +  proof (cases rule: dynmethd_cases)
  1.2106 +    case Static then show ?thesis .
  1.2107 +  next
  1.2108 +    case Overrides 
  1.2109 +    with private show ?thesis 
  1.2110 +      by (auto dest: no_Private_override)
  1.2111 +  qed
  1.2112 +qed
  1.2113 +
  1.2114 +lemma wf_imethds_hiding_objmethdsD: 
  1.2115 +  (assumes     old: "methd G Object sig = Some old" and
  1.2116 +           is_if_I: "is_iface G I" and
  1.2117 +                wf: "wf_prog G" and    
  1.2118 +       not_private: "accmodi old \<noteq> Private" and
  1.2119 +               new: "new \<in> imethds G I sig" 
  1.2120 +  ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
  1.2121 +proof -
  1.2122 +  from wf have ws: "ws_prog G" by simp
  1.2123 +  {
  1.2124 +    fix I i new
  1.2125 +    assume ifI: "iface G I = Some i"
  1.2126 +    assume new: "table_of (imethods i) sig = Some new" 
  1.2127 +    from ifI new not_private wf old  
  1.2128 +    have "?P (I,new)"
  1.2129 +      by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
  1.2130 +            simp del: methd_Object)
  1.2131 +  } note hyp_newmethod = this  
  1.2132 +  from is_if_I ws new 
  1.2133 +  show ?thesis
  1.2134 +  proof (induct rule: ws_interface_induct)
  1.2135 +    case (Step I i)
  1.2136 +    assume ifI: "iface G I = Some i" 
  1.2137 +    assume new: "new \<in> imethds G I sig" 
  1.2138 +    from Step
  1.2139 +    have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)"
  1.2140 +      by auto 
  1.2141 +    from new ifI ws
  1.2142 +    show "?P new"
  1.2143 +    proof (cases rule: imethds_cases)
  1.2144 +      case NewMethod
  1.2145 +      with ifI hyp_newmethod
  1.2146 +      show ?thesis
  1.2147 +	by auto
  1.2148 +    next
  1.2149 +      case (InheritedMethod J)
  1.2150 +      assume "J \<in> set (isuperIfs i)" 
  1.2151 +             "new \<in> imethds G J sig"
  1.2152 +      with hyp 
  1.2153 +      show "?thesis"
  1.2154 +	by auto
  1.2155 +    qed
  1.2156 +  qed
  1.2157 +qed
  1.2158 +
  1.2159 +text {*
  1.2160 +Which dynamic classes are valid to look up a member of a distinct static type?
  1.2161 +We have to distinct class members (named static members in Java) 
  1.2162 +from instance members. Class members are global to all Objects of a class,
  1.2163 +instance members are local to a single Object instance. If a member is
  1.2164 +equipped with the static modifier it is a class member, else it is an 
  1.2165 +instance member.
  1.2166 +The following table gives an overview of the current framework. We assume
  1.2167 +to have a reference with static type statT and a dynamic class dynC. Between
  1.2168 +both of these types the widening relation holds 
  1.2169 +@{term "G\<turnstile>Class dynC\<preceq> statT"}. Unfortunately this ordinary widening relation 
  1.2170 +isn't enough to describe the valid lookup classes, since we must cope the
  1.2171 +special cases of arrays and interfaces,too. If we statically expect an array or
  1.2172 +inteface we may lookup a field or a method in Object which isn't covered in 
  1.2173 +the widening relation.
  1.2174 +\begin{verbatim}
  1.2175 +statT      field         instance method       static (class) method
  1.2176 +------------------------------------------------------------------------
  1.2177 + NullT      /                  /                   /
  1.2178 + Iface      /                dynC                Object
  1.2179 + Class    dynC               dynC                 dynC
  1.2180 + Array      /                Object              Object
  1.2181 +\end{verbatim}
  1.2182 +In most cases we con lookup the member in the dynamic class. But as an
  1.2183 +interface can't declare new static methods, nor an array can define new
  1.2184 +methods at all, we have to lookup methods in the base class Object.
  1.2185 +
  1.2186 +The limitation to classes in the field column is artificial  and comes out
  1.2187 +of the typing rule for the field access (see rule @{text "FVar"} in the 
  1.2188 +welltyping relation @{term "wt"} in theory WellType). 
  1.2189 +I stems out of the fact, that Object
  1.2190 +indeed has no non private fields. So interfaces and arrays can actually
  1.2191 +have no fields at all and a field access would be senseless. (In Java
  1.2192 +interfaces are allowed to declare new fields but in current Bali not!).
  1.2193 +So there is no principal reason why we should not allow Objects to declare
  1.2194 +non private fields. Then we would get the following column:
  1.2195 +\begin{verbatim}
  1.2196 + statT    field
  1.2197 +----------------- 
  1.2198 + NullT      /  
  1.2199 + Iface    Object 
  1.2200 + Class    dynC 
  1.2201 + Array    Object
  1.2202 +\end{verbatim}
  1.2203 +*}
  1.2204 +consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  1.2205 +                        ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
  1.2206 +primrec
  1.2207 +"G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  1.2208 +"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  1.2209 +              = (if static_membr 
  1.2210 +                    then dynC=Object 
  1.2211 +                    else G\<turnstile>Class dynC\<preceq> Iface I)"
  1.2212 +"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  1.2213 +"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  1.2214 +
  1.2215 +lemma valid_lookup_cls_is_class:
  1.2216 + (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
  1.2217 +      ty_statT: "isrtype G statT" and
  1.2218 +            wf: "wf_prog G"
  1.2219 + ) "is_class G dynC"
  1.2220 +proof (cases statT)
  1.2221 +  case NullT
  1.2222 +  with dynC ty_statT show ?thesis
  1.2223 +    by (auto dest: widen_NT2)
  1.2224 +next
  1.2225 +  case (IfaceT I)
  1.2226 +  with dynC wf show ?thesis
  1.2227 +    by (auto dest: implmt_is_class)
  1.2228 +next
  1.2229 +  case (ClassT C)
  1.2230 +  with dynC ty_statT show ?thesis
  1.2231 +    by (auto dest: subcls_is_class2)
  1.2232 +next
  1.2233 +  case (ArrayT T)
  1.2234 +  with dynC wf show ?thesis
  1.2235 +    by (auto)
  1.2236 +qed
  1.2237 +
  1.2238 +declare split_paired_All [simp del] split_paired_Ex [simp del]
  1.2239 +ML_setup {*
  1.2240 +simpset_ref() := simpset() delloop "split_all_tac";
  1.2241 +claset_ref () := claset () delSWrapper "split_all_tac"
  1.2242 +*}
  1.2243 +
  1.2244 +lemma dynamic_mheadsD:   
  1.2245 +"\<lbrakk>emh \<in> mheads G S statT sig;    
  1.2246 +  G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
  1.2247 +  isrtype G statT; wf_prog G
  1.2248 + \<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: 
  1.2249 +          is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh"
  1.2250 +proof - 
  1.2251 +  assume      emh: "emh \<in> mheads G S statT sig"
  1.2252 +  and          wf: "wf_prog G"
  1.2253 +  and   dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)"
  1.2254 +  and      istype: "isrtype G statT"
  1.2255 +  from dynC_Prop istype wf 
  1.2256 +  obtain y where
  1.2257 +    dynC: "class G dynC = Some y" 
  1.2258 +    by (auto dest: valid_lookup_cls_is_class)
  1.2259 +  from emh wf show ?thesis
  1.2260 +  proof (cases rule: mheads_cases)
  1.2261 +    case Class_methd
  1.2262 +    fix statC statDeclC sm
  1.2263 +    assume     statC: "statT = ClassT statC"
  1.2264 +    assume            "accmethd G S statC sig = Some sm"
  1.2265 +    then have     sm: "methd G statC sig = Some sm" 
  1.2266 +      by (blast dest: accmethd_SomeD)  
  1.2267 +    assume eq_mheads: "mhead (mthd sm) = mhd emh"
  1.2268 +    from statC 
  1.2269 +    have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
  1.2270 +      by (simp add: dynlookup_def)
  1.2271 +    from wf statC istype dynC_Prop sm 
  1.2272 +    obtain dm where
  1.2273 +      "dynmethd G statC dynC sig = Some dm"
  1.2274 +      "is_static dm = is_static sm" 
  1.2275 +      "G\<turnstile>resTy dm\<preceq>resTy sm"  
  1.2276 +      by (auto dest!: ws_dynmethd accmethd_SomeD)
  1.2277 +    with dynlookup eq_mheads 
  1.2278 +    show ?thesis 
  1.2279 +      by (cases emh type: *) (auto)
  1.2280 +  next
  1.2281 +    case Iface_methd
  1.2282 +    fix I im
  1.2283 +    assume    statI: "statT = IfaceT I" and
  1.2284 +          eq_mheads: "mthd im = mhd emh" and
  1.2285 +                     "im \<in> accimethds G (pid S) I sig" 
  1.2286 +    then have im: "im \<in> imethds G I sig" 
  1.2287 +      by (blast dest: accimethdsD)
  1.2288 +    with istype statI eq_mheads wf 
  1.2289 +    have not_static_emh: "\<not> is_static emh"
  1.2290 +      by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  1.2291 +    from statI im
  1.2292 +    have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  1.2293 +      by (auto simp add: dynlookup_def dynimethd_def) 
  1.2294 +    from wf dynC_Prop statI istype im not_static_emh 
  1.2295 +    obtain dm where
  1.2296 +      "methd G dynC sig = Some dm"
  1.2297 +      "is_static dm = is_static im" 
  1.2298 +      "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  1.2299 +      by (auto dest: implmt_methd)
  1.2300 +    with dynlookup eq_mheads
  1.2301 +    show ?thesis 
  1.2302 +      by (cases emh type: *) (auto)
  1.2303 +  next
  1.2304 +    case Iface_Object_methd
  1.2305 +    fix I sm
  1.2306 +    assume   statI: "statT = IfaceT I" and
  1.2307 +                sm: "accmethd G S Object sig = Some sm" and 
  1.2308 +         eq_mheads: "mhead (mthd sm) = mhd emh" and
  1.2309 +             nPriv: "accmodi sm \<noteq> Private"
  1.2310 +     show ?thesis 
  1.2311 +     proof (cases "imethds G I sig = {}")
  1.2312 +       case True
  1.2313 +       with statI 
  1.2314 +       have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig"
  1.2315 +	 by (simp add: dynlookup_def dynimethd_def)
  1.2316 +       from wf dynC 
  1.2317 +       have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  1.2318 +	 by (auto intro: subcls_ObjectI)
  1.2319 +       from wf dynC dynC_Prop istype sm subclsObj 
  1.2320 +       obtain dm where
  1.2321 +	 "dynmethd G Object dynC sig = Some dm"
  1.2322 +	 "is_static dm = is_static sm" 
  1.2323 +	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)"  
  1.2324 +	 by (auto dest!: ws_dynmethd accmethd_SomeD 
  1.2325 +                  intro: class_Object [OF wf])
  1.2326 +       with dynlookup eq_mheads
  1.2327 +       show ?thesis 
  1.2328 +	 by (cases emh type: *) (auto)
  1.2329 +     next
  1.2330 +       case False
  1.2331 +       with statI
  1.2332 +       have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  1.2333 +	 by (simp add: dynlookup_def dynimethd_def)
  1.2334 +       from istype statI
  1.2335 +       have "is_iface G I"
  1.2336 +	 by auto
  1.2337 +       with wf sm nPriv False 
  1.2338 +       obtain im where
  1.2339 +	      im: "im \<in> imethds G I sig" and
  1.2340 +	 eq_stat: "is_static im = is_static sm" and
  1.2341 +         resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)"
  1.2342 +	 by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD)
  1.2343 +       from im wf statI istype eq_stat eq_mheads
  1.2344 +       have not_static_sm: "\<not> is_static emh"
  1.2345 +	 by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  1.2346 +       from im wf dynC_Prop dynC istype statI not_static_sm
  1.2347 +       obtain dm where
  1.2348 +	 "methd G dynC sig = Some dm"
  1.2349 +	 "is_static dm = is_static im" 
  1.2350 +	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  1.2351 +	 by (auto dest: implmt_methd)
  1.2352 +       with wf eq_stat resProp dynlookup eq_mheads
  1.2353 +       show ?thesis 
  1.2354 +	 by (cases emh type: *) (auto intro: widen_trans)
  1.2355 +     qed
  1.2356 +  next
  1.2357 +    case Array_Object_methd
  1.2358 +    fix T sm
  1.2359 +    assume statArr: "statT = ArrayT T" and
  1.2360 +                sm: "accmethd G S Object sig = Some sm" and 
  1.2361 +         eq_mheads: "mhead (mthd sm) = mhd emh" 
  1.2362 +    from statArr dynC_Prop wf
  1.2363 +    have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
  1.2364 +      by (auto simp add: dynlookup_def dynmethd_C_C)
  1.2365 +    with sm eq_mheads sm 
  1.2366 +    show ?thesis 
  1.2367 +      by (cases emh type: *) (auto dest: accmethd_SomeD)
  1.2368 +  qed
  1.2369 +qed
  1.2370 +
  1.2371 +(* Tactical version *)
  1.2372 +(*
  1.2373 +lemma dynamic_mheadsD: "  
  1.2374 + \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y;  
  1.2375 +   if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; 
  1.2376 +   isrtype G statT\<rbrakk> \<Longrightarrow>  
  1.2377 +  \<exists>m \<in> dynlookup G statT dynC sig: 
  1.2378 +     static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)"
  1.2379 +apply (drule mheadsD)
  1.2380 +apply safe
  1.2381 +       -- reftype statT is a class  
  1.2382 +apply  (case_tac "\<exists>T. ClassT C = ArrayT T")
  1.2383 +apply    (simp)
  1.2384 +
  1.2385 +apply    (clarsimp simp add: dynlookup_def )
  1.2386 +apply    (frule_tac statC="C" and dynC="dynC"  and sig="sig"  
  1.2387 +         in ws_dynmethd)
  1.2388 +apply      assumption+
  1.2389 +apply    (case_tac "emh")  
  1.2390 +apply    (force dest: accmethd_SomeD)
  1.2391 +
  1.2392 +       -- reftype statT is a interface, method defined in interface 
  1.2393 +apply    (clarsimp simp add: dynlookup_def)
  1.2394 +apply    (drule (1) implmt_methd)
  1.2395 +apply      blast
  1.2396 +apply      blast
  1.2397 +apply    (clarify)  
  1.2398 +apply    (unfold dynimethd_def)
  1.2399 +apply    (rule_tac x="cm" in bexI)
  1.2400 +apply      (case_tac "emh")
  1.2401 +apply      force
  1.2402 +
  1.2403 +apply      force
  1.2404 +
  1.2405 +        -- reftype statT is a interface, method defined in Object 
  1.2406 +apply    (simp add: dynlookup_def)
  1.2407 +apply    (simp only: dynimethd_def)
  1.2408 +apply    (case_tac "imethds G I sig = {}")
  1.2409 +apply       simp
  1.2410 +apply       (frule_tac statC="Object" and dynC="dynC"  and sig="sig"  
  1.2411 +             in ws_dynmethd)
  1.2412 +apply          (blast intro: subcls_ObjectI wf_ws_prog) 
  1.2413 +apply          (blast dest: class_Object)
  1.2414 +apply       (case_tac "emh") 
  1.2415 +apply       (force dest: accmethd_SomeD)
  1.2416 +
  1.2417 +apply       simp
  1.2418 +apply       (subgoal_tac "\<exists> im. im \<in> imethds G I sig") 
  1.2419 +prefer 2      apply blast
  1.2420 +apply       clarify
  1.2421 +apply       (frule (1) implmt_methd)
  1.2422 +apply         simp
  1.2423 +apply         blast  
  1.2424 +apply       (clarify dest!: accmethd_SomeD)
  1.2425 +apply       (frule (4) iface_overrides_Object)
  1.2426 +apply       clarify
  1.2427 +apply       (case_tac emh)
  1.2428 +apply       force
  1.2429 +
  1.2430 +        -- reftype statT is a array
  1.2431 +apply    (simp add: dynlookup_def)
  1.2432 +apply    (case_tac emh)
  1.2433 +apply    (force dest: accmethd_SomeD simp add: dynmethd_def)
  1.2434 +done
  1.2435 +*)
  1.2436 +
  1.2437 +(* ### auf ws_class_induct umstellen *)
  1.2438 +lemma methd_declclass:
  1.2439 +"\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> 
  1.2440 + \<Longrightarrow> methd G (declclass m) sig = Some m"
  1.2441 +proof -
  1.2442 +  assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m"
  1.2443 +  have "wf_prog G  \<longrightarrow> 
  1.2444 +	   (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
  1.2445 +                   \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
  1.2446 +  proof (rule class_rec.induct,intro allI impI)
  1.2447 +    fix G C c m
  1.2448 +    assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
  1.2449 +                     ?P G (super c)"
  1.2450 +    assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  1.2451 +            m: "methd G C sig = Some m"
  1.2452 +    show "methd G (declclass m) sig = Some m"
  1.2453 +    proof (cases "C=Object")
  1.2454 +      case True
  1.2455 +      with wf m show ?thesis by (auto intro: table_of_map_SomeI)
  1.2456 +    next
  1.2457 +      let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  1.2458 +      let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1.2459 +      case False
  1.2460 +      with cls_C wf m
  1.2461 +      have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  1.2462 +	by (simp add: methd_rec)
  1.2463 +      show ?thesis
  1.2464 +      proof (cases "?table sig")
  1.2465 +	case None
  1.2466 +	from this methd_C have "?filter (methd G (super c)) sig = Some m"
  1.2467 +	  by simp
  1.2468 +	moreover
  1.2469 +	from wf cls_C False obtain sup where "class G (super c) = Some sup"
  1.2470 +	  by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1.2471 +	moreover note wf False cls_C hyp
  1.2472 +	ultimately show ?thesis by auto
  1.2473 +      next
  1.2474 +	case Some
  1.2475 +	from this methd_C m show ?thesis by auto 
  1.2476 +      qed
  1.2477 +    qed
  1.2478 +  qed	
  1.2479 +  with asm show ?thesis by auto
  1.2480 +qed
  1.2481 +
  1.2482 +lemma dynmethd_declclass:
  1.2483 + "\<lbrakk>dynmethd G statC dynC sig = Some m;
  1.2484 +   wf_prog G; is_class G statC
  1.2485 +  \<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m"
  1.2486 +by (auto dest: dynmethd_declC)
  1.2487 +
  1.2488 +lemma dynlookup_declC:
  1.2489 + "\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G;
  1.2490 +   is_class G dynC;isrtype G statT
  1.2491 +  \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)"
  1.2492 +by (cases "statT")
  1.2493 +   (auto simp add: dynlookup_def dynimethd_def 
  1.2494 +             dest: methd_declC dynmethd_declC)
  1.2495 +
  1.2496 +lemma dynlookup_Array_declclassD [simp]:
  1.2497 +"\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> 
  1.2498 + \<Longrightarrow> declclass dm = Object"
  1.2499 +proof -
  1.2500 +  assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm"
  1.2501 +  assume wf: "wf_prog G"
  1.2502 +  from wf have ws: "ws_prog G" by auto
  1.2503 +  from wf have is_cls_Obj: "is_class G Object" by auto
  1.2504 +  from dynL wf
  1.2505 +  show ?thesis
  1.2506 +    by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws]
  1.2507 +                 dest: methd_Object_SomeD)
  1.2508 +qed   
  1.2509 +  
  1.2510 +declare split_paired_All [simp del] split_paired_Ex [simp del]
  1.2511 +ML_setup {*
  1.2512 +simpset_ref() := simpset() delloop "split_all_tac";
  1.2513 +claset_ref () := claset () delSWrapper "split_all_tac"
  1.2514 +*}
  1.2515 +
  1.2516 +lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
  1.2517 +  dt=empty_dt \<longrightarrow> (case T of 
  1.2518 +                     Inl T \<Rightarrow> is_type (prg E) T 
  1.2519 +                   | Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))"
  1.2520 +apply (unfold empty_dt_def)
  1.2521 +apply (erule wt.induct)
  1.2522 +apply (auto split del: split_if_asm simp del: snd_conv 
  1.2523 +            simp add: is_acc_class_def is_acc_type_def)
  1.2524 +apply    (erule typeof_empty_is_type)
  1.2525 +apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1, 
  1.2526 +        force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
  1.2527 +apply  (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
  1.2528 +apply  (drule_tac [2] accfield_fields) 
  1.2529 +apply  (frule class_Object)
  1.2530 +apply  (auto dest: accmethd_rT_is_type 
  1.2531 +                   imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type]
  1.2532 +             dest!:accimethdsD
  1.2533 +             simp del: class_Object
  1.2534 +             simp add: is_acc_type_def
  1.2535 +    )
  1.2536 +done
  1.2537 +declare split_paired_All [simp] split_paired_Ex [simp]
  1.2538 +ML_setup {*
  1.2539 +claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  1.2540 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  1.2541 +*}
  1.2542 +
  1.2543 +lemma ty_expr_is_type: 
  1.2544 +"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  1.2545 +by (auto dest!: wt_is_type)
  1.2546 +lemma ty_var_is_type: 
  1.2547 +"\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  1.2548 +by (auto dest!: wt_is_type)
  1.2549 +lemma ty_exprs_is_type: 
  1.2550 +"\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))"
  1.2551 +by (auto dest!: wt_is_type)
  1.2552 +
  1.2553 +
  1.2554 +lemma static_mheadsD: 
  1.2555 + "\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; 
  1.2556 +   invmode (mhd emh) e \<noteq> IntVir 
  1.2557 +  \<rbrakk> \<Longrightarrow> \<exists>m. (   (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m)
  1.2558 +               \<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> 
  1.2559 +          declrefT emh = ClassT (declclass m) \<and>  mhead (mthd m) = (mhd emh)"
  1.2560 +apply (subgoal_tac "is_static emh \<or> e = Super")
  1.2561 +defer apply (force simp add: invmode_def)
  1.2562 +apply (frule  ty_expr_is_type)
  1.2563 +apply   simp
  1.2564 +apply (case_tac "is_static emh")
  1.2565 +apply  (frule (1) mheadsD)
  1.2566 +apply  clarsimp
  1.2567 +apply  safe
  1.2568 +apply    blast
  1.2569 +apply   (auto dest!: imethds_wf_mhead
  1.2570 +                     accmethd_SomeD 
  1.2571 +                     accimethdsD
  1.2572 +              simp add: accObjectmheads_def Objectmheads_def)
  1.2573 +
  1.2574 +apply  (erule wt_elim_cases)
  1.2575 +apply  (force simp add: cmheads_def)
  1.2576 +done
  1.2577 +
  1.2578 +lemma wt_MethdI:  
  1.2579 +"\<lbrakk>methd G C sig = Some m; wf_prog G;  
  1.2580 +  class G C = Some c\<rbrakk> \<Longrightarrow>  
  1.2581 + \<exists>T. \<lparr>prg=G,cls=(declclass m),
  1.2582 +      lcl=\<lambda> k. 
  1.2583 +          (case k of
  1.2584 +             EName e 
  1.2585 +             \<Rightarrow> (case e of 
  1.2586 +                   VNam v 
  1.2587 +                   \<Rightarrow> (table_of (lcls (mbody (mthd m)))
  1.2588 +                                ((pars (mthd m))[\<mapsto>](parTs sig))) v
  1.2589 +                 | Res \<Rightarrow> Some (resTy (mthd m)))
  1.2590 +           | This \<Rightarrow> if is_static m then None else Some (Class (declclass m)))
  1.2591 +     \<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
  1.2592 +apply (frule (2) methd_wf_mdecl, clarify)
  1.2593 +apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
  1.2594 +done
  1.2595 +
  1.2596 +subsection "accessibility concerns"
  1.2597 +
  1.2598 +lemma mheads_type_accessible:
  1.2599 + "\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk>
  1.2600 + \<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)"
  1.2601 +by (erule mheads_cases)
  1.2602 +   (auto dest: accmethd_SomeD accessible_from_commonD accimethdsD)
  1.2603 +
  1.2604 +lemma static_to_dynamic_accessible_from:
  1.2605 +"\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> 
  1.2606 + \<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC"
  1.2607 +proof (induct rule: accessible_fromR.induct)
  1.2608 +qed (auto intro: dyn_accessible_fromR.intros 
  1.2609 +                 member_of_to_member_in
  1.2610 +                 static_to_dynamic_overriding)
  1.2611 +
  1.2612 +lemma static_to_dynamic_accessible_from:
  1.2613 + (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  1.2614 +          subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  1.2615 +                wf: "wf_prog G"
  1.2616 + ) "G\<turnstile>m in dynC dyn_accessible_from accC"
  1.2617 +proof - 
  1.2618 +  from stat_acc subclseq 
  1.2619 +  show ?thesis (is "?Dyn_accessible m")
  1.2620 +  proof (induct rule: accessible_fromR.induct)
  1.2621 +    case (immediate statC m)
  1.2622 +    then show "?Dyn_accessible m"
  1.2623 +      by (blast intro: dyn_accessible_fromR.immediate
  1.2624 +                       member_inI
  1.2625 +                       permits_acc_inheritance)
  1.2626 +  next
  1.2627 +    case (overriding _ _ m)
  1.2628 +    with wf show "?Dyn_accessible m"
  1.2629 +      by (blast intro: dyn_accessible_fromR.overriding
  1.2630 +                       member_inI
  1.2631 +                       static_to_dynamic_overriding  
  1.2632 +                       rtrancl_trancl_trancl 
  1.2633 +                       static_to_dynamic_accessible_from)
  1.2634 +  qed
  1.2635 +qed
  1.2636 +
  1.2637 +lemma dynmethd_member_in:
  1.2638 + (assumes    m: "dynmethd G statC dynC sig = Some m" and
  1.2639 +   iscls_statC: "is_class G statC" and
  1.2640 +            wf: "wf_prog G"
  1.2641 + ) "G\<turnstile>Methd sig m member_in dynC"
  1.2642 +proof -
  1.2643 +  from m 
  1.2644 +  have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  1.2645 +    by (auto simp add: dynmethd_def)
  1.2646 +  from subclseq iscls_statC 
  1.2647 +  have iscls_dynC: "is_class G dynC"
  1.2648 +    by (rule subcls_is_class2)
  1.2649 +  from  iscls_dynC iscls_statC wf m
  1.2650 +  have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and>
  1.2651 +        methd G (declclass m) sig = Some m" 
  1.2652 +    by - (drule dynmethd_declC, auto)
  1.2653 +  with wf 
  1.2654 +  show ?thesis
  1.2655 +    by (auto intro: member_inI dest: methd_member_of)
  1.2656 +qed
  1.2657 +
  1.2658 +lemma dynmethd_access_prop:
  1.2659 +  (assumes statM: "methd G statC sig = Some statM" and
  1.2660 +        stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
  1.2661 +            dynM: "dynmethd G statC dynC sig = Some dynM" and
  1.2662 +              wf: "wf_prog G" 
  1.2663 +   ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2664 +proof -
  1.2665 +  from wf have ws: "ws_prog G" ..
  1.2666 +  from dynM 
  1.2667 +  have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  1.2668 +    by (auto simp add: dynmethd_def)
  1.2669 +  from stat_acc 
  1.2670 +  have is_cls_statC: "is_class G statC"
  1.2671 +    by (auto dest: accessible_from_commonD member_of_is_classD)
  1.2672 +  with subclseq 
  1.2673 +  have is_cls_dynC: "is_class G dynC"
  1.2674 +    by (rule subcls_is_class2)
  1.2675 +  from is_cls_statC statM wf 
  1.2676 +  have member_statC: "G\<turnstile>Methd sig statM member_of statC"
  1.2677 +    by (auto intro: methd_member_of)
  1.2678 +  from stat_acc 
  1.2679 +  have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)"
  1.2680 +    by (auto dest: accessible_from_commonD)
  1.2681 +  from statM subclseq is_cls_statC ws 
  1.2682 +  show ?thesis
  1.2683 +  proof (cases rule: dynmethd_cases)
  1.2684 +    case Static
  1.2685 +    assume dynmethd: "dynmethd G statC dynC sig = Some statM"
  1.2686 +    with dynM have eq_dynM_statM: "dynM=statM" 
  1.2687 +      by simp
  1.2688 +    with stat_acc subclseq wf 
  1.2689 +    show ?thesis
  1.2690 +      by (auto intro: static_to_dynamic_accessible_from)
  1.2691 +  next
  1.2692 +    case (Overrides newM)
  1.2693 +    assume dynmethd: "dynmethd G statC dynC sig = Some newM"
  1.2694 +    assume override: "G,sig\<turnstile>newM overrides statM"
  1.2695 +    assume      neq: "newM\<noteq>statM"
  1.2696 +    from dynmethd dynM 
  1.2697 +    have eq_dynM_newM: "dynM=newM" 
  1.2698 +      by simp
  1.2699 +    from dynmethd eq_dynM_newM wf is_cls_statC
  1.2700 +    have "G\<turnstile>Methd sig dynM member_in dynC"
  1.2701 +      by (auto intro: dynmethd_member_in)
  1.2702 +    moreover
  1.2703 +    from subclseq
  1.2704 +    have "G\<turnstile>dynC\<prec>\<^sub>C statC"
  1.2705 +    proof (cases rule: subclseq_cases)
  1.2706 +      case Eq
  1.2707 +      assume "dynC=statC"
  1.2708 +      moreover
  1.2709 +      from is_cls_statC obtain c
  1.2710 +	where "class G statC = Some c"
  1.2711 +	by auto
  1.2712 +      moreover 
  1.2713 +      note statM ws dynmethd 
  1.2714 +      ultimately
  1.2715 +      have "newM=statM" 
  1.2716 +	by (auto simp add: dynmethd_C_C)
  1.2717 +      with neq show ?thesis 
  1.2718 +	by (contradiction)
  1.2719 +    next
  1.2720 +      case Subcls show ?thesis .
  1.2721 +    qed 
  1.2722 +    moreover
  1.2723 +    from stat_acc wf 
  1.2724 +    have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC"
  1.2725 +      by (blast intro: static_to_dynamic_accessible_from)
  1.2726 +    moreover
  1.2727 +    note override eq_dynM_newM
  1.2728 +    ultimately show ?thesis
  1.2729 +      by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.overriding)
  1.2730 +  qed
  1.2731 +qed
  1.2732 +
  1.2733 +lemma implmt_methd_access:
  1.2734 +(fixes accC::qtname
  1.2735 + assumes iface_methd: "imethds G I sig \<noteq> {}" and
  1.2736 +           implements: "G\<turnstile>dynC\<leadsto>I"  and
  1.2737 +               isif_I: "is_iface G I" and
  1.2738 +                   wf: "wf_prog G" 
  1.2739 + ) "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
  1.2740 +            G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2741 +proof -
  1.2742 +  from implements 
  1.2743 +  have iscls_dynC: "is_class G dynC" by (rule implmt_is_class)
  1.2744 +  from iface_methd
  1.2745 +  obtain im
  1.2746 +    where "im \<in> imethds G I sig"
  1.2747 +    by auto
  1.2748 +  with wf implements isif_I 
  1.2749 +  obtain dynM 
  1.2750 +    where dynM: "methd G dynC sig = Some dynM" and
  1.2751 +           pub: "accmodi dynM = Public"
  1.2752 +    by (blast dest: implmt_methd)
  1.2753 +  with iscls_dynC wf
  1.2754 +  have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2755 +    by (auto intro!: dyn_accessible_fromR.immediate 
  1.2756 +              intro: methd_member_of member_of_to_member_in
  1.2757 +                     simp add: permits_acc_def)
  1.2758 +  with dynM    
  1.2759 +  show ?thesis
  1.2760 +    by blast
  1.2761 +qed
  1.2762 +
  1.2763 +corollary implmt_dynimethd_access:
  1.2764 +(fixes accC::qtname
  1.2765 + assumes iface_methd: "imethds G I sig \<noteq> {}" and
  1.2766 +           implements: "G\<turnstile>dynC\<leadsto>I"  and
  1.2767 +               isif_I: "is_iface G I" and
  1.2768 +                   wf: "wf_prog G" 
  1.2769 + ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
  1.2770 +            G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2771 +proof -
  1.2772 +  from iface_methd
  1.2773 +  have "dynimethd G I dynC sig = methd G dynC sig"
  1.2774 +    by (simp add: dynimethd_def)
  1.2775 +  with iface_methd implements isif_I wf 
  1.2776 +  show ?thesis
  1.2777 +    by (simp only:)
  1.2778 +       (blast intro: implmt_methd_access)
  1.2779 +qed
  1.2780 +
  1.2781 +lemma dynlookup_access_prop:
  1.2782 + (assumes emh: "emh \<in> mheads G accC statT sig" and
  1.2783 +         dynM: "dynlookup G statT dynC sig = Some dynM" and
  1.2784 +    dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
  1.2785 +    isT_statT: "isrtype G statT" and
  1.2786 +           wf: "wf_prog G"
  1.2787 + ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2788 +proof -
  1.2789 +  from emh wf
  1.2790 +  have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
  1.2791 +    by (rule mheads_type_accessible)
  1.2792 +  from dynC_prop isT_statT wf
  1.2793 +  have iscls_dynC: "is_class G dynC"
  1.2794 +    by (rule valid_lookup_cls_is_class)
  1.2795 +  from emh dynC_prop isT_statT wf dynM
  1.2796 +  have eq_static: "is_static emh = is_static dynM"
  1.2797 +    by (auto dest: dynamic_mheadsD)
  1.2798 +  from emh wf show ?thesis
  1.2799 +  proof (cases rule: mheads_cases)
  1.2800 +    case (Class_methd statC _ statM)
  1.2801 +    assume statT: "statT = ClassT statC"
  1.2802 +    assume "accmethd G accC statC sig = Some statM"
  1.2803 +    then have    statM: "methd G statC sig = Some statM" and
  1.2804 +              stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC"
  1.2805 +      by (auto dest: accmethd_SomeD)
  1.2806 +    from dynM statT
  1.2807 +    have dynM': "dynmethd G statC dynC sig = Some dynM"
  1.2808 +      by (simp add: dynlookup_def) 
  1.2809 +    from statM stat_acc wf dynM'
  1.2810 +    show ?thesis
  1.2811 +      by (auto dest!: dynmethd_access_prop)
  1.2812 +  next
  1.2813 +    case (Iface_methd I im)
  1.2814 +    then have iface_methd: "imethds G I sig \<noteq> {}" and
  1.2815 +                 statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 
  1.2816 +      by (auto dest: accimethdsD)
  1.2817 +    assume   statT: "statT = IfaceT I"
  1.2818 +    assume      im: "im \<in>  accimethds G (pid accC) I sig"
  1.2819 +    assume eq_mhds: "mthd im = mhd emh"
  1.2820 +    from dynM statT
  1.2821 +    have dynM': "dynimethd G I dynC sig = Some dynM"
  1.2822 +      by (simp add: dynlookup_def)
  1.2823 +    from isT_statT statT 
  1.2824 +    have isif_I: "is_iface G I"
  1.2825 +      by simp
  1.2826 +    show ?thesis
  1.2827 +    proof (cases "is_static emh")
  1.2828 +      case False
  1.2829 +      with statT dynC_prop 
  1.2830 +      have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT"
  1.2831 +	by simp
  1.2832 +      from statT widen_dynC
  1.2833 +      have implmnt: "G\<turnstile>dynC\<leadsto>I"
  1.2834 +	by auto    
  1.2835 +      from eq_static False 
  1.2836 +      have not_static_dynM: "\<not> is_static dynM" 
  1.2837 +	by simp
  1.2838 +      from iface_methd implmnt isif_I wf dynM'
  1.2839 +      show ?thesis
  1.2840 +	by - (drule implmt_dynimethd_access, auto)
  1.2841 +    next
  1.2842 +      case True
  1.2843 +      assume "is_static emh"
  1.2844 +      moreover
  1.2845 +      from wf isT_statT statT im 
  1.2846 +      have "\<not> is_static im"
  1.2847 +	by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead)
  1.2848 +      moreover note eq_mhds
  1.2849 +      ultimately show ?thesis
  1.2850 +	by (cases emh) auto
  1.2851 +    qed
  1.2852 +  next
  1.2853 +    case (Iface_Object_methd I statM)
  1.2854 +    assume statT: "statT = IfaceT I"
  1.2855 +    assume "accmethd G accC Object sig = Some statM"
  1.2856 +    then have    statM: "methd G Object sig = Some statM" and
  1.2857 +              stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  1.2858 +      by (auto dest: accmethd_SomeD)
  1.2859 +    assume not_Private_statM: "accmodi statM \<noteq> Private"
  1.2860 +    assume eq_mhds: "mhead (mthd statM) = mhd emh"
  1.2861 +    from iscls_dynC wf
  1.2862 +    have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  1.2863 +      by (auto intro: subcls_ObjectI)
  1.2864 +    show ?thesis
  1.2865 +    proof (cases "imethds G I sig = {}")
  1.2866 +      case True
  1.2867 +      from dynM statT True
  1.2868 +      have dynM': "dynmethd G Object dynC sig = Some dynM"
  1.2869 +	by (simp add: dynlookup_def dynimethd_def)
  1.2870 +      from statT  
  1.2871 +      have "G\<turnstile>RefT statT \<preceq>Class Object"
  1.2872 +	by auto
  1.2873 +      with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT 
  1.2874 +        wf dynM' eq_static dynC_prop  
  1.2875 +      show ?thesis
  1.2876 +	by - (drule dynmethd_access_prop,force+) 
  1.2877 +    next
  1.2878 +      case False
  1.2879 +      then obtain im where
  1.2880 +	im: "im \<in>  imethds G I sig"
  1.2881 +	by auto
  1.2882 +      have not_static_emh: "\<not> is_static emh"
  1.2883 +      proof -
  1.2884 +	from im statM statT isT_statT wf not_Private_statM 
  1.2885 +	have "is_static im = is_static statM"
  1.2886 +	  by (auto dest: wf_imethds_hiding_objmethdsD)
  1.2887 +	with wf isT_statT statT im 
  1.2888 +	have "\<not> is_static statM"
  1.2889 +	  by (auto dest: wf_prog_idecl imethds_wf_mhead)
  1.2890 +	with eq_mhds
  1.2891 +	show ?thesis  
  1.2892 +	  by (cases emh) auto
  1.2893 +      qed
  1.2894 +      with statT dynC_prop
  1.2895 +      have implmnt: "G\<turnstile>dynC\<leadsto>I"
  1.2896 +	by simp
  1.2897 +      with isT_statT statT
  1.2898 +      have isif_I: "is_iface G I"
  1.2899 +	by simp
  1.2900 +      from dynM statT
  1.2901 +      have dynM': "dynimethd G I dynC sig = Some dynM"
  1.2902 +	by (simp add: dynlookup_def) 
  1.2903 +      from False implmnt isif_I wf dynM'
  1.2904 +      show ?thesis
  1.2905 +	by - (drule implmt_dynimethd_access, auto)
  1.2906 +    qed
  1.2907 +  next
  1.2908 +    case (Array_Object_methd T statM)
  1.2909 +    assume statT: "statT = ArrayT T"
  1.2910 +    assume "accmethd G accC Object sig = Some statM"
  1.2911 +    then have    statM: "methd G Object sig = Some statM" and
  1.2912 +              stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  1.2913 +      by (auto dest: accmethd_SomeD)
  1.2914 +    from statT dynC_prop
  1.2915 +    have dynC_Obj: "dynC = Object" 
  1.2916 +      by simp
  1.2917 +    then
  1.2918 +    have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object"
  1.2919 +      by simp
  1.2920 +    from dynM statT    
  1.2921 +    have dynM': "dynmethd G Object dynC sig = Some dynM"
  1.2922 +      by (simp add: dynlookup_def)
  1.2923 +    from statM statT_acc stat_acc dynM' wf widen_dynC_Obj  
  1.2924 +         statT isT_statT  
  1.2925 +    show ?thesis   
  1.2926 +      by - (drule dynmethd_access_prop, simp+) 
  1.2927 +  qed
  1.2928 +qed
  1.2929 +
  1.2930 +lemma dynlookup_access:
  1.2931 + (assumes emh: "emh \<in> mheads G accC statT sig" and
  1.2932 +    dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
  1.2933 +    isT_statT: "isrtype G statT" and
  1.2934 +           wf: "wf_prog G"
  1.2935 + ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
  1.2936 +            G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  1.2937 +proof - 
  1.2938 +  from dynC_prop isT_statT wf
  1.2939 +  have is_cls_dynC: "is_class G dynC"
  1.2940 +    by (auto dest: valid_lookup_cls_is_class)
  1.2941 +  with emh wf dynC_prop isT_statT
  1.2942 +  obtain dynM where 
  1.2943 +    "dynlookup G statT dynC sig = Some dynM"
  1.2944 +    by - (drule dynamic_mheadsD,auto)
  1.2945 +  with  emh dynC_prop isT_statT wf
  1.2946 +  show ?thesis 
  1.2947 +    by (blast intro: dynlookup_access_prop)
  1.2948 +qed
  1.2949 +
  1.2950 +lemma stat_overrides_Package_old: 
  1.2951 +(assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
  1.2952 +          accmodi_new: "accmodi new = Package" and
  1.2953 +                   wf: "wf_prog G "
  1.2954 +) "accmodi old = Package"
  1.2955 +proof -
  1.2956 +  from stat_override wf 
  1.2957 +  have "accmodi old \<le> accmodi new"
  1.2958 +    by (auto dest: wf_prog_stat_overridesD)
  1.2959 +  with stat_override accmodi_new show ?thesis
  1.2960 +    by (cases "accmodi old") (auto dest: no_Private_stat_override 
  1.2961 +                                   dest: acc_modi_le_Dests)
  1.2962 +qed
  1.2963 +
  1.2964 +text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
  1.2965 +Without it. it is easy to leaf the Package!
  1.2966 +*}
  1.2967 +lemma dyn_accessible_Package:
  1.2968 + "\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package;
  1.2969 +   wf_prog G\<rbrakk>
  1.2970 +  \<Longrightarrow> pid accC = pid (declclass m)"
  1.2971 +proof -
  1.2972 +  assume wf: "wf_prog G "
  1.2973 +  assume accessible: "G \<turnstile> m in C dyn_accessible_from accC"
  1.2974 +  then show "accmodi m = Package 
  1.2975 +            \<Longrightarrow> pid accC = pid (declclass m)"
  1.2976 +    (is "?Pack m \<Longrightarrow> ?P m")
  1.2977 +  proof (induct rule: dyn_accessible_fromR.induct)
  1.2978 +    case (immediate C m)
  1.2979 +    assume "G\<turnstile>m member_in C"
  1.2980 +           "G \<turnstile> m in C permits_acc_to accC"
  1.2981 +           "accmodi m = Package"      
  1.2982 +    then show "?P m"
  1.2983 +      by (auto simp add: permits_acc_def)
  1.2984 +  next
  1.2985 +    case (overriding declC C new newm old Sup)
  1.2986 +    assume member_new: "G \<turnstile> new member_in C" and
  1.2987 +                  new: "new = (declC, mdecl newm)" and
  1.2988 +             override: "G \<turnstile> (declC, newm) overrides old" and
  1.2989 +         subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
  1.2990 +              acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and
  1.2991 +                  hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and
  1.2992 +          accmodi_new: "accmodi new = Package"
  1.2993 +    from override accmodi_new new wf 
  1.2994 +    have accmodi_old: "accmodi old = Package"  
  1.2995 +      by (auto dest: overrides_Package_old)
  1.2996 +    with hyp 
  1.2997 +    have P_sup: "?P (methdMembr old)"
  1.2998 +      by (simp)
  1.2999 +    from wf override new accmodi_old accmodi_new
  1.3000 +    have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
  1.3001 +      by (auto dest: dyn_override_Package)
  1.3002 +    with eq_pid_new_old P_sup show "?P new"
  1.3003 +      by auto
  1.3004 +  qed
  1.3005 +qed
  1.3006 +
  1.3007 +end
  1.3008 \ No newline at end of file