src/HOL/Bali/WellForm.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12893 cbb4dc5e6478
child 12937 0c4fd7529467
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
     1 (*  Title:      HOL/Bali/WellForm.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb and Norbert Schirmer
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Well-formedness of Java programs *}
     8 
     9 theory WellForm = WellType:
    10 
    11 text {*
    12 For static checks on expressions and statements, see WellType.thy
    13 
    14 improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
    15 \begin{itemize}
    16 \item a method implementing or overwriting another method may have a result 
    17       type that widens to the result type of the other method 
    18       (instead of identical type)
    19 \item if a method hides another method (both methods have to be static!)
    20   there are no restrictions to the result type 
    21   since the methods have to be static and there is no dynamic binding of 
    22   static methods
    23 \item if an interface inherits more than one method with the same signature, the
    24   methods need not have identical return types
    25 \end{itemize}
    26 simplifications:
    27 \begin{itemize}
    28 \item Object and standard exceptions are assumed to be declared like normal 
    29       classes
    30 \end{itemize}
    31 *}
    32 
    33 section "well-formed field declarations"
    34 text  {* well-formed field declaration (common part for classes and interfaces),
    35         cf. 8.3 and (9.3) *}
    36 
    37 constdefs
    38   wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
    39  "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
    40 
    41 lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    42 apply (unfold wf_fdecl_def)
    43 apply simp
    44 done
    45 
    46 
    47 
    48 section "well-formed method declarations"
    49   (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
    50   (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
    51 
    52 text {*
    53 A method head is wellformed if:
    54 \begin{itemize}
    55 \item the signature and the method head agree in the number of parameters
    56 \item all types of the parameters are visible
    57 \item the result type is visible
    58 \item the parameter names are unique
    59 \end{itemize} 
    60 *}
    61 constdefs
    62   wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
    63  "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
    64 			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
    65                             is_acc_type G P (resTy mh) \<and>
    66 			    \<spacespace> distinct (pars mh)"
    67 
    68 
    69 text {*
    70 A method declaration is wellformed if:
    71 \begin{itemize}
    72 \item the method head is wellformed
    73 \item the names of the local variables are unique
    74 \item the types of the local variables must be accessible
    75 \item the local variables don't shadow the parameters
    76 \item the class of the method is defined
    77 \item the body statement is welltyped with respect to the
    78       modified environment of local names, were the local variables, 
    79       the parameters the special result variable (Res) and This are assoziated
    80       with there types. 
    81 \end{itemize}
    82 *}
    83 
    84 constdefs
    85   wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
    86  "wf_mdecl G C \<equiv> 
    87       \<lambda>(sig,m).
    88 	  wf_mhead G (pid C) sig (mhead m) \<and> 
    89           unique (lcls (mbody m)) \<and> 
    90           (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
    91 	  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and>
    92           is_class G C \<and>
    93           \<lparr>prg=G,cls=C,
    94            lcl=\<lambda> k. 
    95                (case k of
    96                   EName e 
    97                   \<Rightarrow> (case e of 
    98                         VNam v 
    99                         \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   100                       | Res \<Rightarrow> Some (resTy m))
   101 	        | This \<Rightarrow> if is_static m then None else Some (Class C))
   102           \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>"
   103 
   104 lemma wf_mheadI: 
   105 "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
   106   is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
   107   wf_mhead G P sig m"
   108 apply (unfold wf_mhead_def)
   109 apply (simp (no_asm_simp))
   110 done
   111 
   112 lemma wf_mdeclI: "\<lbrakk>  
   113   wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
   114   (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 
   115   \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
   116   is_class G C;
   117   \<lparr>prg=G,cls=C,
   118    lcl=\<lambda> k. 
   119        (case k of
   120           EName e 
   121           \<Rightarrow> (case e of 
   122                 VNam v 
   123                 \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   124               | Res \<Rightarrow> Some (resTy m))
   125         | This \<Rightarrow> if is_static m then None else Some (Class C))
   126   \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>
   127   \<rbrakk> \<Longrightarrow>  
   128   wf_mdecl G C (sig,m)"
   129 apply (unfold wf_mdecl_def)
   130 apply simp
   131 done
   132 
   133 
   134 lemma wf_mdeclD1: 
   135 "wf_mdecl G C (sig,m) \<Longrightarrow>  
   136    wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and>  
   137   (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 
   138   (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)"
   139 apply (unfold wf_mdecl_def)
   140 apply auto
   141 done
   142 
   143 lemma wf_mdecl_bodyD: 
   144 "wf_mdecl G C (sig,m) \<Longrightarrow>  
   145  (\<exists>T. \<lparr>prg=G,cls=C,
   146        lcl = \<lambda> k. 
   147          (case k of
   148             EName e 
   149             \<Rightarrow> (case e of 
   150                 VNam v \<Rightarrow> (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
   151                 | Res  \<Rightarrow> Some (resTy m))
   152           | This \<Rightarrow> if is_static m then None else Some (Class C))
   153        \<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> G\<turnstile>T\<preceq>(resTy m))"
   154 apply (unfold wf_mdecl_def)
   155 apply clarify
   156 apply (rule_tac x="(resTy m)" in exI)
   157 apply (unfold wf_mhead_def)
   158 apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
   159 done
   160 
   161 
   162 (*
   163 lemma static_Object_methodsE [elim!]: 
   164  "\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R"
   165 apply (unfold wf_mdecl_def)
   166 apply auto
   167 done
   168 *)
   169 
   170 lemma rT_is_acc_type: 
   171   "wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)"
   172 apply (unfold wf_mhead_def)
   173 apply auto
   174 done
   175 
   176 section "well-formed interface declarations"
   177   (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
   178 
   179 text {*
   180 A interface declaration is wellformed if:
   181 \begin{itemize}
   182 \item the interface hierarchy is wellstructured
   183 \item there is no class with the same name
   184 \item the method heads are wellformed and not static and have Public access
   185 \item the methods are uniquely named
   186 \item all superinterfaces are accessible
   187 \item the result type of a method overriding a method of Object widens to the
   188       result type of the overridden method.
   189       Shadowing static methods is forbidden.
   190 \item the result type of a method overriding a set of methods defined in the
   191       superinterfaces widens to each of the corresponding result types
   192 \end{itemize}
   193 *}
   194 constdefs
   195   wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool"
   196  "wf_idecl G \<equiv> 
   197     \<lambda>(I,i). 
   198         ws_idecl G I (isuperIfs i) \<and> 
   199 	\<not>is_class G I \<and>
   200 	(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
   201                                      \<not>is_static mh \<and>
   202                                       accmodi mh = Public) \<and>
   203 	unique (imethods i) \<and>
   204         (\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and>
   205         (table_of (imethods i)
   206           hiding (methd G Object)
   207           under  (\<lambda> new old. accmodi old \<noteq> Private)
   208           entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
   209                              is_static new = is_static old)) \<and> 
   210         (o2s \<circ> table_of (imethods i) 
   211                hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
   212 	       entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
   213 
   214 lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
   215   wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
   216 apply (unfold wf_idecl_def)
   217 apply auto
   218 done
   219 
   220 lemma wf_idecl_hidings: 
   221 "wf_idecl G (I, i) \<Longrightarrow> 
   222   (\<lambda>s. o2s (table_of (imethods i) s)) 
   223   hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
   224   entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
   225 apply (unfold wf_idecl_def o_def)
   226 apply simp
   227 done
   228 
   229 lemma wf_idecl_hiding:
   230 "wf_idecl G (I, i) \<Longrightarrow> 
   231  (table_of (imethods i)
   232            hiding (methd G Object)
   233            under  (\<lambda> new old. accmodi old \<noteq> Private)
   234            entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
   235                               is_static new = is_static old))"
   236 apply (unfold wf_idecl_def)
   237 apply simp
   238 done
   239 
   240 lemma wf_idecl_supD: 
   241 "\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 
   242  \<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+"
   243 apply (unfold wf_idecl_def ws_idecl_def)
   244 apply auto
   245 done
   246 
   247 section "well-formed class declarations"
   248   (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
   249    class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
   250 
   251 text {*
   252 A class declaration is wellformed if:
   253 \begin{itemize}
   254 \item there is no interface with the same name
   255 \item all superinterfaces are accessible and for all methods implementing 
   256       an interface method the result type widens to the result type of 
   257       the interface method, the method is not static and offers at least 
   258       as much access 
   259       (this actually means that the method has Public access, since all 
   260       interface methods have public access)
   261 \item all field declarations are wellformed and the field names are unique
   262 \item all method declarations are wellformed and the method names are unique
   263 \item the initialization statement is welltyped
   264 \item the classhierarchy is wellstructured
   265 \item Unless the class is Object:
   266       \begin{itemize}
   267       \item the superclass is accessible
   268       \item for all methods overriding another method (of a superclass )the
   269             result type widens to the result type of the overridden method,
   270             the access modifier of the new method provides at least as much
   271             access as the overwritten one.
   272       \item for all methods hiding a method (of a superclass) the hidden 
   273             method must be static and offer at least as much access rights.
   274             Remark: In contrast to the Java Language Specification we don't
   275             restrict the result types of the method
   276             (as in case of overriding), because there seems to be no reason,
   277             since there is no dynamic binding of static methods.
   278             (cf. 8.4.6.3 vs. 15.12.1).
   279             Stricly speaking the restrictions on the access rights aren't 
   280             necessary to, since the static type and the access rights 
   281             together determine which method is to be called statically. 
   282             But if a class gains more then one static method with the 
   283             same signature due to inheritance, it is confusing when the 
   284             method selection depends on the access rights only: 
   285             e.g.
   286               Class C declares static public method foo().
   287               Class D is subclass of C and declares static method foo()
   288               with default package access.
   289               D.foo() ? if this call is in the same package as D then
   290                         foo of class D is called, otherwise foo of class C.
   291       \end{itemize}
   292 
   293 \end{itemize}
   294 *}
   295 (* to Table *)
   296 constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
   297                                  ("_ entails _" 20)
   298 "t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
   299 
   300 lemma entailsD:
   301  "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
   302 by (simp add: entails_def)
   303 
   304 lemma empty_entails[simp]: "empty entails P"
   305 by (simp add: entails_def)
   306 
   307 constdefs
   308  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
   309 "wf_cdecl G \<equiv> 
   310    \<lambda>(C,c).
   311       \<not>is_iface G C \<and>
   312       (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   313         (\<forall>s. \<forall> im \<in> imethds G I s.
   314       	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
   315       	                             \<not> is_static cm \<and>
   316                                      accmodi im \<le> accmodi cm))) \<and>
   317       (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
   318       (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
   319       \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
   320       (C \<noteq> Object \<longrightarrow> 
   321             (is_acc_class G (pid C) (super c) \<and>
   322             (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   323              entails (\<lambda> new. \<forall> old sig. 
   324                        (G,sig\<turnstile>new overrides\<^sub>S old 
   325                         \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
   326                              accmodi old \<le> accmodi new \<and>
   327       	                     \<not>is_static old)) \<and>
   328                        (G,sig\<turnstile>new hides old 
   329                          \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   330       	                      is_static old)))) 
   331             ))"
   332 
   333 (*
   334 constdefs
   335  wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
   336 "wf_cdecl G \<equiv> 
   337    \<lambda>(C,c).
   338       \<not>is_iface G C \<and>
   339       (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
   340         (\<forall>s. \<forall> im \<in> imethds G I s.
   341       	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and>
   342       	                             \<not> is_static cm \<and>
   343                                      accmodi im \<le> accmodi cm))) \<and>
   344       (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
   345       (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
   346       \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
   347       (C \<noteq> Object \<longrightarrow> 
   348             (is_acc_class G (pid C) (super c) \<and>
   349             (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   350               hiding methd G (super c)
   351               under (\<lambda> new old. G\<turnstile>new overrides old)
   352               entails (\<lambda> new old. 
   353                            (G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and>
   354                             accmodi old \<le> accmodi new \<and>
   355       	                   \<not> is_static old)))  \<and>
   356             (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   357               hiding methd G (super c)
   358               under (\<lambda> new old. G\<turnstile>new hides old)
   359               entails (\<lambda> new old. is_static old \<and> 
   360                                   accmodi old \<le> accmodi new))  \<and>
   361             (table_of (cfields c) hiding accfield G C (super c)
   362               entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))"
   363 *)
   364 
   365 lemma wf_cdecl_unique: 
   366 "wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)"
   367 apply (unfold wf_cdecl_def)
   368 apply auto
   369 done
   370 
   371 lemma wf_cdecl_fdecl: 
   372 "\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f"
   373 apply (unfold wf_cdecl_def)
   374 apply auto
   375 done
   376 
   377 lemma wf_cdecl_mdecl: 
   378 "\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m"
   379 apply (unfold wf_cdecl_def)
   380 apply auto
   381 done
   382 
   383 lemma wf_cdecl_impD: 
   384 "\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 
   385 \<Longrightarrow> is_acc_iface G (pid C) I \<and>  
   386     (\<forall>s. \<forall>im \<in> imethds G I s.  
   387         (\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and>
   388                                    accmodi im \<le> accmodi cm))"
   389 apply (unfold wf_cdecl_def)
   390 apply auto
   391 done
   392 
   393 lemma wf_cdecl_supD: 
   394 "\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow>  
   395   is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 
   396    (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
   397     entails (\<lambda> new. \<forall> old sig. 
   398                  (G,sig\<turnstile>new overrides\<^sub>S old 
   399                   \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
   400                        accmodi old \<le> accmodi new \<and>
   401                        \<not>is_static old)) \<and>
   402                  (G,sig\<turnstile>new hides old 
   403                    \<longrightarrow> (accmodi old \<le> accmodi new \<and>
   404                         is_static old))))"
   405 apply (unfold wf_cdecl_def ws_cdecl_def)
   406 apply auto
   407 done
   408 
   409 
   410 lemma wf_cdecl_overrides_SomeD:
   411 "\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
   412   G,sig\<turnstile>(C,newM) overrides\<^sub>S old
   413 \<rbrakk> \<Longrightarrow>  G\<turnstile>resTy newM\<preceq>resTy old \<and>
   414        accmodi old \<le> accmodi newM \<and>
   415        \<not> is_static old" 
   416 apply (drule (1) wf_cdecl_supD)
   417 apply (clarify)
   418 apply (drule entailsD)
   419 apply   (blast intro: table_of_map_SomeI)
   420 apply (drule_tac x="old" in spec)
   421 apply (auto dest: overrides_eq_sigD simp add: msig_def)
   422 done
   423 
   424 lemma wf_cdecl_hides_SomeD:
   425 "\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
   426   G,sig\<turnstile>(C,newM) hides old
   427 \<rbrakk> \<Longrightarrow>  accmodi old \<le> access newM \<and>
   428        is_static old" 
   429 apply (drule (1) wf_cdecl_supD)
   430 apply (clarify)
   431 apply (drule entailsD)
   432 apply   (blast intro: table_of_map_SomeI)
   433 apply (drule_tac x="old" in spec)
   434 apply (auto dest: hides_eq_sigD simp add: msig_def)
   435 done
   436 
   437 lemma wf_cdecl_wt_init: 
   438  "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
   439 apply (unfold wf_cdecl_def)
   440 apply auto
   441 done
   442 
   443 
   444 section "well-formed programs"
   445   (* well-formed program, cf. 8.1, 9.1 *)
   446 
   447 text {*
   448 A program declaration is wellformed if:
   449 \begin{itemize}
   450 \item the class ObjectC of Object is defined
   451 \item every method of has an access modifier distinct from Package. This is
   452       necessary since every interface automatically inherits from Object.  
   453       We must know, that every time a Object method is "overriden" by an 
   454       interface method this is also overriden by the class implementing the
   455       the interface (see @{text "implement_dynmethd and class_mheadsD"})
   456 \item all standard Exceptions are defined
   457 \item all defined interfaces are wellformed
   458 \item all defined classes are wellformed
   459 \end{itemize}
   460 *}
   461 constdefs
   462   wf_prog  :: "prog \<Rightarrow> bool"
   463  "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
   464 	         ObjectC \<in> set cs \<and> 
   465                 (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
   466                 (\<forall>xn. SXcptC xn \<in> set cs) \<and>
   467 		(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
   468 		(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
   469 
   470 lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
   471 apply (unfold wf_prog_def Let_def)
   472 apply simp
   473 apply (fast dest: map_of_SomeD)
   474 done
   475 
   476 lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)"
   477 apply (unfold wf_prog_def Let_def)
   478 apply simp
   479 apply (fast dest: map_of_SomeD)
   480 done
   481 
   482 lemma wf_prog_Object_mdecls:
   483 "wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)"
   484 apply (unfold wf_prog_def Let_def)
   485 apply simp
   486 done
   487 
   488 lemma wf_prog_acc_superD:
   489  "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 
   490   \<Longrightarrow> is_acc_class G (pid C) (super c)"
   491 by (auto dest: wf_prog_cdecl wf_cdecl_supD)
   492 
   493 lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G"
   494 apply (unfold wf_prog_def Let_def)
   495 apply (rule ws_progI)
   496 apply  (simp_all (no_asm))
   497 apply  (auto simp add: is_acc_class_def is_acc_iface_def 
   498              dest!: wf_idecl_supD wf_cdecl_supD )+
   499 done
   500 
   501 lemma class_Object [simp]: 
   502 "wf_prog G \<Longrightarrow> 
   503   class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
   504                                   init=Skip,super=arbitrary,superIfs=[]\<rparr>"
   505 apply (unfold wf_prog_def Let_def ObjectC_def)
   506 apply (fast dest!: map_of_SomeI)
   507 done
   508 
   509 lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object =  
   510   table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)"
   511 apply (subst methd_rec)
   512 apply (auto simp add: Let_def)
   513 done
   514 
   515 lemma wf_prog_Object_methd:
   516 "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package"
   517 by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 
   518 
   519 lemma wf_prog_Object_is_public[intro]:
   520  "wf_prog G \<Longrightarrow> is_public G Object"
   521 by (auto simp add: is_public_def dest: class_Object)
   522 
   523 lemma class_SXcpt [simp]: 
   524 "wf_prog G \<Longrightarrow> 
   525   class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   526                                    init=Skip,
   527                                    super=if xn = Throwable then Object 
   528                                                            else SXcpt Throwable,
   529                                    superIfs=[]\<rparr>"
   530 apply (unfold wf_prog_def Let_def SXcptC_def)
   531 apply (fast dest!: map_of_SomeI)
   532 done
   533 
   534 lemma wf_ObjectC [simp]: 
   535 	"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls)
   536   (wf_mdecl G Object) \<and> unique Object_mdecls)"
   537 apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
   538 apply (simp (no_asm))
   539 done
   540 
   541 lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object"
   542 apply (simp (no_asm_simp))
   543 done
   544  
   545 lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object"
   546 apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
   547                                accessible_in_RefT_simp)
   548 done
   549 
   550 lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)"
   551 apply (simp (no_asm_simp))
   552 done
   553 
   554 lemma SXcpt_is_acc_class [simp,elim!]: 
   555 "wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)"
   556 apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
   557                                accessible_in_RefT_simp)
   558 done
   559 
   560 lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []"
   561 by (force intro: fields_emptyI)
   562 
   563 lemma accfield_Object [simp]: 
   564  "wf_prog G \<Longrightarrow> accfield G S Object = empty"
   565 apply (unfold accfield_def)
   566 apply (simp (no_asm_simp) add: Let_def)
   567 done
   568 
   569 lemma fields_Throwable [simp]: 
   570  "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []"
   571 by (force intro: fields_emptyI)
   572 
   573 lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []"
   574 apply (case_tac "xn = Throwable")
   575 apply  (simp (no_asm_simp))
   576 by (force intro: fields_emptyI)
   577 
   578 lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim]
   579 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"
   580 apply (erule (2) widen_trans)
   581 done
   582 
   583 lemma Xcpt_subcls_Throwable [simp]: 
   584 "wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
   585 apply (rule SXcpt_subcls_Throwable_lemma)
   586 apply auto
   587 done
   588 
   589 lemma unique_fields: 
   590  "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)"
   591 apply (erule ws_unique_fields)
   592 apply  (erule wf_ws_prog)
   593 apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
   594 done
   595 
   596 lemma fields_mono: 
   597 "\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 
   598   is_class G D; wf_prog G\<rbrakk> 
   599    \<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f"
   600 apply (rule map_of_SomeI)
   601 apply  (erule (1) unique_fields)
   602 apply (erule (1) map_of_SomeD [THEN fields_mono_lemma])
   603 apply (erule wf_ws_prog)
   604 done
   605 
   606 
   607 lemma fields_is_type [elim]: 
   608 "\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   609       is_type G (type f)"
   610 apply (frule wf_ws_prog)
   611 apply (force dest: fields_declC [THEN conjunct1] 
   612                    wf_prog_cdecl [THEN wf_cdecl_fdecl]
   613              simp add: wf_fdecl_def2 is_acc_type_def)
   614 done
   615 
   616 lemma imethds_wf_mhead [rule_format (no_asm)]: 
   617 "\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow>  
   618   wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 
   619   \<not> is_static m \<and> accmodi m = Public"
   620 apply (frule wf_ws_prog)
   621 apply (drule (2) imethds_declI [THEN conjunct1])
   622 apply clarify
   623 apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption)
   624 apply (drule wf_idecl_mhead)
   625 apply (erule map_of_SomeD)
   626 apply (cases m, simp)
   627 done
   628 
   629 lemma methd_wf_mdecl: 
   630  "\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow>  
   631   G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 
   632   wf_mdecl G (declclass m) (sig,(mthd m))"
   633 apply (frule wf_ws_prog)
   634 apply (drule (1) methd_declC)
   635 apply  fast
   636 apply clarsimp
   637 apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
   638 done
   639 
   640 (*
   641 This lemma doesn't hold!
   642 lemma methd_rT_is_acc_type: 
   643 "\<lbrakk>wf_prog G;methd G C C sig = Some (D,m);
   644     class G C = Some y\<rbrakk>
   645 \<Longrightarrow> is_acc_type G (pid C) (resTy m)"
   646 The result Type is only visible in the scope of defining class D 
   647 "is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C!
   648 (The same is true for the type of pramaters of a method)
   649 *)
   650 
   651 
   652 lemma methd_rT_is_type: 
   653 "\<lbrakk>wf_prog G;methd G C sig = Some m;
   654     class G C = Some y\<rbrakk>
   655 \<Longrightarrow> is_type G (resTy m)"
   656 apply (drule (2) methd_wf_mdecl)
   657 apply clarify
   658 apply (drule wf_mdeclD1)
   659 apply clarify
   660 apply (drule rT_is_acc_type)
   661 apply (cases m, simp add: is_acc_type_def)
   662 done
   663 
   664 lemma accmethd_rT_is_type:
   665 "\<lbrakk>wf_prog G;accmethd G S C sig = Some m;
   666     class G C = Some y\<rbrakk>
   667 \<Longrightarrow> is_type G (resTy m)"
   668 by (auto simp add: accmethd_def  
   669          intro: methd_rT_is_type)
   670 
   671 lemma methd_Object_SomeD:
   672 "\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 
   673  \<Longrightarrow> declclass m = Object"
   674 by (auto dest: class_Object simp add: methd_rec )
   675 
   676 lemma wf_imethdsD: 
   677  "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
   678  \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
   679 proof -
   680   assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
   681   have "wf_prog G \<longrightarrow> 
   682          (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
   683                   \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
   684   proof (rule iface_rec.induct,intro allI impI)
   685     fix G I i im
   686     assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
   687                  \<longrightarrow> ?P G J"
   688     assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
   689            im: "im \<in> imethds G I sig" 
   690     show "\<not>is_static im \<and> accmodi im = Public" 
   691     proof -
   692       let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
   693       let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
   694       from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
   695 	by (simp add: imethds_rec)
   696       from wf if_I have 
   697 	wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)"
   698 	by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
   699       from wf if_I have
   700 	"\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public"
   701 	by (auto dest!: wf_prog_idecl wf_idecl_mhead)
   702       then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
   703                          \<longrightarrow>  \<not> is_static im \<and> accmodi im = Public"
   704 	by (auto dest!: table_of_Some_in_set)
   705       show ?thesis
   706 	proof (cases "?new sig = {}")
   707 	  case True
   708 	  from True wf wf_supI if_I imethds hyp 
   709 	  show ?thesis by (auto simp del:  split_paired_All)  
   710 	next
   711 	  case False
   712 	  from False wf wf_supI if_I imethds new_ok hyp 
   713 	  show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
   714 	qed
   715       qed
   716     qed
   717   with asm show ?thesis by (auto simp del: split_paired_All)
   718 qed
   719 
   720 lemma wf_prog_hidesD:
   721  (assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G") 
   722    "accmodi old \<le> accmodi new \<and>
   723     is_static old"
   724 proof -
   725   from hides 
   726   obtain c where 
   727     clsNew: "class G (declclass new) = Some c" and
   728     neqObj: "declclass new \<noteq> Object"
   729     by (auto dest: hidesD declared_in_classD)
   730   with hides obtain newM oldM where
   731     newM: "table_of (methods c) (msig new) = Some newM" and 
   732      new: "new = (declclass new,(msig new),newM)" and
   733      old: "old = (declclass old,(msig old),oldM)" and
   734           "msig new = msig old"
   735     by (cases new,cases old) 
   736        (auto dest: hidesD 
   737          simp add: cdeclaredmethd_def declared_in_def)
   738   with hides 
   739   have hides':
   740         "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)"
   741     by auto
   742   from clsNew wf 
   743   have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   744   note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
   745   with new old 
   746   show ?thesis
   747     by (cases new, cases old) auto
   748 qed
   749 
   750 text {* Compare this lemma about static  
   751 overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 
   752 dynamic overriding @{term "G \<turnstile>new overrides old"}. 
   753 Conforming result types and restrictions on the access modifiers of the old 
   754 and the new method are not part of the predicate for static overriding. But
   755 they are enshured in a wellfromed program.  Dynamic overriding has 
   756 no restrictions on the access modifiers but enforces confrom result types 
   757 as precondition. But with some efford we can guarantee the access modifier
   758 restriction for dynamic overriding, too. See lemma 
   759 @{text wf_prog_dyn_override_prop}.
   760 *}
   761 lemma wf_prog_stat_overridesD:
   762  (assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G") 
   763    "G\<turnstile>resTy new\<preceq>resTy old \<and>
   764     accmodi old \<le> accmodi new \<and>
   765     \<not> is_static old"
   766 proof -
   767   from stat_override 
   768   obtain c where 
   769     clsNew: "class G (declclass new) = Some c" and
   770     neqObj: "declclass new \<noteq> Object"
   771     by (auto dest: stat_overrides_commonD declared_in_classD)
   772   with stat_override obtain newM oldM where
   773     newM: "table_of (methods c) (msig new) = Some newM" and 
   774      new: "new = (declclass new,(msig new),newM)" and
   775      old: "old = (declclass old,(msig old),oldM)" and
   776           "msig new = msig old"
   777     by (cases new,cases old) 
   778        (auto dest: stat_overrides_commonD 
   779          simp add: cdeclaredmethd_def declared_in_def)
   780   with stat_override 
   781   have stat_override':
   782         "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
   783     by auto
   784   from clsNew wf 
   785   have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   786   note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
   787   with new old 
   788   show ?thesis
   789     by (cases new, cases old) auto
   790 qed
   791     
   792 lemma static_to_dynamic_overriding: 
   793   (assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G")
   794    "G\<turnstile>new overrides old"
   795 proof -
   796   from stat_override 
   797   show ?thesis (is "?Overrides new old")
   798   proof (induct)
   799     case (Direct new old superNew)
   800     then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 
   801       by (rule stat_overridesR.Direct)
   802     from stat_override wf
   803     have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and
   804       not_static_old: "\<not> is_static old" 
   805       by (auto dest: wf_prog_stat_overridesD)  
   806     have not_private_new: "accmodi new \<noteq> Private"
   807     proof -
   808       from stat_override 
   809       have "accmodi old \<noteq> Private"
   810 	by (rule no_Private_stat_override)
   811       moreover
   812       from stat_override wf
   813       have "accmodi old \<le> accmodi new"
   814 	by (auto dest: wf_prog_stat_overridesD)
   815       ultimately
   816       show ?thesis
   817 	by (auto dest: acc_modi_bottom)
   818     qed
   819     with Direct resTy_widen not_static_old 
   820     show "?Overrides new old" 
   821       by (auto intro: overridesR.Direct) 
   822   next
   823     case (Indirect inter new old)
   824     then show "?Overrides new old" 
   825       by (blast intro: overridesR.Indirect) 
   826   qed
   827 qed
   828 
   829 lemma non_Package_instance_method_inheritance:
   830 (assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
   831              accmodi_old: "accmodi old \<noteq> Package" and 
   832          instance_method: "\<not> is_static old" and
   833                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
   834             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
   835                       wf: "wf_prog G"
   836 ) "G\<turnstile>Method old member_of C \<or>
   837    (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and>  G\<turnstile>Method new member_of C)"
   838 proof -
   839   from wf have ws: "ws_prog G" by auto
   840   from old_declared have iscls_declC_old: "is_class G (declclass old)"
   841     by (auto simp add: declared_in_def cdeclaredmethd_def)
   842   from subcls have  iscls_C: "is_class G C"
   843     by (blast dest:  subcls_is_class)
   844   from iscls_C ws old_inheritable subcls 
   845   show ?thesis (is "?P C old")
   846   proof (induct rule: ws_class_induct')
   847     case Object
   848     assume "G\<turnstile>Object\<prec>\<^sub>C declclass old"
   849     then show "?P Object old"
   850       by blast
   851   next
   852     case (Subcls C c)
   853     assume cls_C: "class G C = Some c" and 
   854        neq_C_Obj: "C \<noteq> Object" and
   855              hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 
   856                    G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and
   857      inheritable: "G \<turnstile>Method old inheritable_in pid C" and
   858          subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
   859     from cls_C neq_C_Obj  
   860     have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 
   861       by (rule subcls1I)
   862     from wf cls_C neq_C_Obj
   863     have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
   864       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
   865     {
   866       fix old
   867       assume    member_super: "G\<turnstile>Method old member_of (super c)"
   868       assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
   869       assume instance_method: "\<not> is_static old"
   870       from member_super
   871       have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
   872        by (cases old) (auto dest: member_of_declC)
   873       have "?P C old"
   874       proof (cases "G\<turnstile>mid (msig old) undeclared_in C")
   875 	case True
   876 	with inheritable super accessible_super member_super
   877 	have "G\<turnstile>Method old member_of C"
   878 	  by (cases old) (auto intro: members.Inherited)
   879 	then show ?thesis
   880 	  by auto
   881       next
   882 	case False
   883 	then obtain new_member where
   884 	     "G\<turnstile>new_member declared_in C" and
   885              "mid (msig old) = memberid new_member"
   886           by (auto dest: not_undeclared_declared)
   887 	then obtain new where
   888 	          new: "G\<turnstile>Method new declared_in C" and
   889                eq_sig: "msig old = msig new" and
   890 	    declC_new: "declclass new = C" 
   891 	  by (cases new_member) auto
   892 	then have member_new: "G\<turnstile>Method new member_of C"
   893 	  by (cases new) (auto intro: members.Immediate)
   894 	from declC_new super member_super
   895 	have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
   896 	  by (auto dest!: member_of_subclseq_declC
   897 	            dest: r_into_trancl intro: trancl_rtrancl_trancl)
   898 	show ?thesis
   899 	proof (cases "is_static new")
   900 	  case False
   901 	  with eq_sig declC_new new old_declared inheritable
   902 	       super member_super subcls_new_old
   903 	  have "G\<turnstile>new overrides\<^sub>S old"
   904 	    by (auto intro!: stat_overridesR.Direct)
   905 	  with member_new show ?thesis
   906 	    by blast
   907 	next
   908 	  case True
   909 	  with eq_sig declC_new subcls_new_old new old_declared inheritable
   910 	  have "G\<turnstile>new hides old"
   911 	    by (auto intro: hidesI)    
   912 	  with wf 
   913 	  have "is_static old"
   914 	    by (blast dest: wf_prog_hidesD)
   915 	  with instance_method
   916 	  show ?thesis
   917 	    by (contradiction)
   918 	qed
   919       qed
   920     } note hyp_member_super = this
   921     from subclsC cls_C 
   922     have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
   923       by (rule subcls_superD)
   924     then
   925     show "?P C old"
   926     proof (cases rule: subclseq_cases) 
   927       case Eq
   928       assume "super c = declclass old"
   929       with old_declared 
   930       have "G\<turnstile>Method old member_of (super c)" 
   931 	by (cases old) (auto intro: members.Immediate)
   932       with inheritable instance_method 
   933       show ?thesis
   934 	by (blast dest: hyp_member_super)
   935     next
   936       case Subcls
   937       assume "G\<turnstile>super c\<prec>\<^sub>C declclass old"
   938       moreover
   939       from inheritable accmodi_old
   940       have "G \<turnstile>Method old inheritable_in pid (super c)"
   941 	by (cases "accmodi old") (auto simp add: inheritable_in_def)
   942       ultimately
   943       have "?P (super c) old"
   944 	by (blast dest: hyp)
   945       then show ?thesis
   946       proof
   947 	assume "G \<turnstile>Method old member_of super c"
   948 	with inheritable instance_method
   949 	show ?thesis
   950 	  by (blast dest: hyp_member_super)
   951       next
   952 	assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c"
   953 	then obtain super_new where
   954 	  super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
   955             super_new_member:  "G \<turnstile>Method super_new member_of super c"
   956 	  by blast
   957 	from super_new_override wf
   958 	have "accmodi old \<le> accmodi super_new"
   959 	  by (auto dest: wf_prog_stat_overridesD)
   960 	with inheritable accmodi_old
   961 	have "G \<turnstile>Method super_new inheritable_in pid C"
   962 	  by (auto simp add: inheritable_in_def 
   963 	              split: acc_modi.splits
   964                        dest: acc_modi_le_Dests)
   965 	moreover
   966 	from super_new_override 
   967 	have "\<not> is_static super_new"
   968 	  by (auto dest: stat_overrides_commonD)
   969 	moreover
   970 	note super_new_member
   971 	ultimately have "?P C super_new"
   972 	  by (auto dest: hyp_member_super)
   973 	then show ?thesis
   974 	proof 
   975 	  assume "G \<turnstile>Method super_new member_of C"
   976 	  with super_new_override
   977 	  show ?thesis
   978 	    by blast
   979 	next
   980 	  assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
   981                   G \<turnstile>Method new member_of C"
   982 	  with super_new_override show ?thesis
   983 	    by (blast intro: stat_overridesR.Indirect) 
   984 	qed
   985       qed
   986     qed
   987   qed
   988 qed
   989 
   990 lemma non_Package_instance_method_inheritance_cases [consumes 6,
   991          case_names Inheritance Overriding]:
   992 (assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
   993              accmodi_old: "accmodi old \<noteq> Package" and 
   994          instance_method: "\<not> is_static old" and
   995                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
   996             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
   997                       wf: "wf_prog G" and
   998              inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
   999              overriding:  "\<And> new. 
  1000                            \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
  1001                            \<Longrightarrow> P"
  1002 ) "P"
  1003 proof -
  1004   from old_inheritable accmodi_old instance_method subcls old_declared wf 
  1005        inheritance overriding
  1006   show ?thesis
  1007     by (auto dest: non_Package_instance_method_inheritance)
  1008 qed
  1009 
  1010 lemma dynamic_to_static_overriding:
  1011 (assumes dyn_override: "G\<turnstile> new overrides old" and
  1012           accmodi_old: "accmodi old \<noteq> Package" and
  1013                    wf: "wf_prog G"
  1014 ) "G\<turnstile> new overrides\<^sub>S old"  
  1015 proof - 
  1016   from dyn_override accmodi_old
  1017   show ?thesis (is "?Overrides new old")
  1018   proof (induct rule: overridesR.induct)
  1019     case (Direct new old)
  1020     assume   new_declared: "G\<turnstile>Method new declared_in declclass new"
  1021     assume eq_sig_new_old: "msig new = msig old"
  1022     assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
  1023     assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and
  1024            "accmodi old \<noteq> Package" and
  1025            "\<not> is_static old" and
  1026            "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and
  1027            "G\<turnstile>Method old declared_in declclass old" 
  1028     from this wf
  1029     show "?Overrides new old"
  1030     proof (cases rule: non_Package_instance_method_inheritance_cases)
  1031       case Inheritance
  1032       assume "G \<turnstile>Method old member_of declclass new"
  1033       then have "G\<turnstile>mid (msig old) undeclared_in declclass new"
  1034       proof cases
  1035 	case Immediate 
  1036 	with subcls_new_old wf show ?thesis 	
  1037 	  by (auto dest: subcls_irrefl)
  1038       next
  1039 	case Inherited
  1040 	then show ?thesis
  1041 	  by (cases old) auto
  1042       qed
  1043       with eq_sig_new_old new_declared
  1044       show ?thesis
  1045 	by (cases old,cases new) (auto dest!: declared_not_undeclared)
  1046     next
  1047       case (Overriding new') 
  1048       assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old"
  1049       then have "msig new' = msig old"
  1050 	by (auto dest: stat_overrides_commonD)
  1051       with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
  1052 	by simp
  1053       assume "G \<turnstile>Method new' member_of declclass new"
  1054       then show ?thesis
  1055       proof (cases)
  1056 	case Immediate
  1057 	then have declC_new: "declclass new' = declclass new" 
  1058 	  by auto
  1059 	from Immediate 
  1060 	have "G\<turnstile>Method new' declared_in declclass new"
  1061 	  by (cases new') auto
  1062 	with new_declared eq_sig_new_new' declC_new 
  1063 	have "new=new'"
  1064 	  by (cases new, cases new') (auto dest: unique_declared_in) 
  1065 	with stat_override_new'
  1066 	show ?thesis
  1067 	  by simp
  1068       next
  1069 	case Inherited
  1070 	then have "G\<turnstile>mid (msig new') undeclared_in declclass new"
  1071 	  by (cases new') (auto)
  1072 	with eq_sig_new_new' new_declared
  1073 	show ?thesis
  1074 	  by (cases new,cases new') (auto dest!: declared_not_undeclared)
  1075       qed
  1076     qed
  1077   next
  1078     case (Indirect inter new old)
  1079     assume accmodi_old: "accmodi old \<noteq> Package"
  1080     assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old"
  1081     with accmodi_old 
  1082     have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old"
  1083       by blast
  1084     moreover 
  1085     assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter"
  1086     moreover
  1087     have "accmodi inter \<noteq> Package"
  1088     proof -
  1089       from stat_override_inter_old wf 
  1090       have "accmodi old \<le> accmodi inter"
  1091 	by (auto dest: wf_prog_stat_overridesD)
  1092       with stat_override_inter_old accmodi_old
  1093       show ?thesis
  1094 	by (auto dest!: no_Private_stat_override
  1095                  split: acc_modi.splits 
  1096 	         dest: acc_modi_le_Dests)
  1097     qed
  1098     ultimately show "?Overrides new old"
  1099       by (blast intro: stat_overridesR.Indirect)
  1100   qed
  1101 qed
  1102 
  1103 lemma wf_prog_dyn_override_prop:
  1104  (assumes dyn_override: "G \<turnstile> new overrides old" and
  1105                     wf: "wf_prog G"
  1106  ) "accmodi old \<le> accmodi new"
  1107 proof (cases "accmodi old = Package")
  1108   case True
  1109   note old_Package = this
  1110   show ?thesis
  1111   proof (cases "accmodi old \<le> accmodi new")
  1112     case True then show ?thesis .
  1113   next
  1114     case False
  1115     with old_Package 
  1116     have "accmodi new = Private"
  1117       by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
  1118     with dyn_override 
  1119     show ?thesis
  1120       by (auto dest: overrides_commonD)
  1121   qed    
  1122 next
  1123   case False
  1124   with dyn_override wf
  1125   have "G \<turnstile> new overrides\<^sub>S old"
  1126     by (blast intro: dynamic_to_static_overriding)
  1127   with wf 
  1128   show ?thesis
  1129    by (blast dest: wf_prog_stat_overridesD)
  1130 qed 
  1131 
  1132 lemma overrides_Package_old: 
  1133 (assumes dyn_override: "G \<turnstile> new overrides old" and 
  1134           accmodi_new: "accmodi new = Package" and
  1135                    wf: "wf_prog G "
  1136 ) "accmodi old = Package"
  1137 proof (cases "accmodi old")
  1138   case Private
  1139   with dyn_override show ?thesis
  1140     by (simp add: no_Private_override)
  1141 next
  1142   case Package
  1143   then show ?thesis .
  1144 next
  1145   case Protected
  1146   with dyn_override wf
  1147   have "G \<turnstile> new overrides\<^sub>S old"
  1148     by (auto intro: dynamic_to_static_overriding)
  1149   with wf 
  1150   have "accmodi old \<le> accmodi new"
  1151     by (auto dest: wf_prog_stat_overridesD)
  1152   with Protected accmodi_new
  1153   show ?thesis
  1154     by (simp add: less_acc_def le_acc_def)
  1155 next
  1156   case Public
  1157   with dyn_override wf
  1158   have "G \<turnstile> new overrides\<^sub>S old"
  1159     by (auto intro: dynamic_to_static_overriding)
  1160   with wf 
  1161   have "accmodi old \<le> accmodi new"
  1162     by (auto dest: wf_prog_stat_overridesD)
  1163   with Public accmodi_new
  1164   show ?thesis
  1165     by (simp add: less_acc_def le_acc_def)
  1166 qed
  1167 
  1168 lemma dyn_override_Package:
  1169  (assumes dyn_override: "G \<turnstile> new overrides old" and
  1170           accmodi_old: "accmodi old = Package" and 
  1171           accmodi_new: "accmodi new = Package" and
  1172                     wf: "wf_prog G"
  1173  ) "pid (declclass old) = pid (declclass new)"
  1174 proof - 
  1175   from dyn_override accmodi_old accmodi_new
  1176   show ?thesis (is "?EqPid old new")
  1177   proof (induct rule: overridesR.induct)
  1178     case (Direct new old)
  1179     assume "accmodi old = Package"
  1180            "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1181     then show "pid (declclass old) =  pid (declclass new)"
  1182       by (auto simp add: inheritable_in_def)
  1183   next
  1184     case (Indirect inter new old)
  1185     assume accmodi_old: "accmodi old = Package" and
  1186            accmodi_new: "accmodi new = Package" 
  1187     assume "G \<turnstile> new overrides inter"
  1188     with accmodi_new wf
  1189     have "accmodi inter = Package"
  1190       by  (auto intro: overrides_Package_old)
  1191     with Indirect
  1192     show "pid (declclass old) =  pid (declclass new)"
  1193       by auto
  1194   qed
  1195 qed
  1196 
  1197 lemma dyn_override_Package_escape:
  1198  (assumes dyn_override: "G \<turnstile> new overrides old" and
  1199           accmodi_old: "accmodi old = Package" and 
  1200          outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
  1201                     wf: "wf_prog G"
  1202  ) "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
  1203              pid (declclass old) = pid (declclass inter) \<and>
  1204              Protected \<le> accmodi inter"
  1205 proof -
  1206   from dyn_override accmodi_old outside_pack
  1207   show ?thesis (is "?P new old")
  1208   proof (induct rule: overridesR.induct)
  1209     case (Direct new old)
  1210     assume accmodi_old: "accmodi old = Package"
  1211     assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1212     assume "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1213     with accmodi_old 
  1214     have "pid (declclass old) = pid (declclass new)"
  1215       by (simp add: inheritable_in_def)
  1216     with outside_pack 
  1217     show "?P new old"
  1218       by (contradiction)
  1219   next
  1220     case (Indirect inter new old)
  1221     assume accmodi_old: "accmodi old = Package"
  1222     assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1223     assume override_new_inter: "G \<turnstile> new overrides inter"
  1224     assume override_inter_old: "G \<turnstile> inter overrides old"
  1225     assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 
  1226                            pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk>
  1227                            \<Longrightarrow> ?P new inter"
  1228     assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 
  1229                            pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk>
  1230                            \<Longrightarrow> ?P inter old"
  1231     show "?P new old"
  1232     proof (cases "pid (declclass old) = pid (declclass inter)")
  1233       case True
  1234       note same_pack_old_inter = this
  1235       show ?thesis
  1236       proof (cases "pid (declclass inter) = pid (declclass new)")
  1237 	case True
  1238 	with same_pack_old_inter outside_pack
  1239 	show ?thesis
  1240 	  by auto
  1241       next
  1242 	case False
  1243 	note diff_pack_inter_new = this
  1244 	show ?thesis
  1245 	proof (cases "accmodi inter = Package")
  1246 	  case True
  1247 	  with diff_pack_inter_new hyp_new_inter  
  1248 	  obtain newinter where
  1249 	    over_new_newinter: "G \<turnstile> new overrides newinter" and
  1250             over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
  1251             eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
  1252             accmodi_newinter: "Protected \<le> accmodi newinter"
  1253 	    by auto
  1254 	  from over_newinter_inter override_inter_old
  1255 	  have "G\<turnstile>newinter overrides old"
  1256 	    by (rule overridesR.Indirect)
  1257 	  moreover
  1258 	  from eq_pid same_pack_old_inter 
  1259 	  have "pid (declclass old) = pid (declclass newinter)"
  1260 	    by simp
  1261 	  moreover
  1262 	  note over_new_newinter accmodi_newinter
  1263 	  ultimately show ?thesis
  1264 	    by blast
  1265 	next
  1266 	  case False
  1267 	  with override_new_inter
  1268 	  have "Protected \<le> accmodi inter"
  1269 	    by (cases "accmodi inter") (auto dest: no_Private_override)
  1270 	  with override_new_inter override_inter_old same_pack_old_inter
  1271 	  show ?thesis
  1272 	    by blast
  1273 	qed
  1274       qed
  1275     next
  1276       case False
  1277       with accmodi_old hyp_inter_old
  1278       obtain newinter where
  1279 	over_inter_newinter: "G \<turnstile> inter overrides newinter" and
  1280           over_newinter_old: "G \<turnstile> newinter overrides old" and 
  1281                 eq_pid: "pid (declclass old) = pid (declclass newinter)" and
  1282 	accmodi_newinter: "Protected \<le> accmodi newinter"
  1283 	by auto
  1284       from override_new_inter over_inter_newinter 
  1285       have "G \<turnstile> new overrides newinter"
  1286 	by (rule overridesR.Indirect)
  1287       with eq_pid over_newinter_old accmodi_newinter
  1288       show ?thesis
  1289 	by blast
  1290     qed
  1291   qed
  1292 qed
  1293 
  1294 lemma declclass_widen[rule_format]: 
  1295  "wf_prog G 
  1296  \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1297  \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1298 proof (rule class_rec.induct,intro allI impI)
  1299   fix G C c m
  1300   assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
  1301                \<longrightarrow> ?P G (super c)"
  1302   assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  1303          m:  "methd G C sig = Some m"
  1304   show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
  1305   proof (cases "C=Object")
  1306     case True 
  1307     with wf m show ?thesis by (simp add: methd_Object_SomeD)
  1308   next
  1309     let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  1310     let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1311     case False 
  1312     with cls_C wf m
  1313     have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  1314       by (simp add: methd_rec)
  1315     show ?thesis
  1316     proof (cases "?table sig")
  1317       case None
  1318       from this methd_C have "?filter (methd G (super c)) sig = Some m"
  1319 	by simp
  1320       moreover
  1321       from wf cls_C False obtain sup where "class G (super c) = Some sup"
  1322 	by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1323       moreover note wf False cls_C  
  1324       ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  
  1325 	by (auto intro: Hyp [rule_format])
  1326       moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I)
  1327       ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
  1328     next
  1329       case Some
  1330       from this wf False cls_C methd_C show ?thesis by auto
  1331     qed
  1332   qed
  1333 qed
  1334 
  1335 lemma declclass_methd_Object: 
  1336  "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object"
  1337 by auto
  1338 
  1339 lemma methd_declaredD: 
  1340  "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 
  1341   \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1342 proof -
  1343   assume    wf: "wf_prog G"
  1344   then have ws: "ws_prog G" ..
  1345   assume  clsC: "is_class G C"
  1346   from clsC ws 
  1347   show "methd G C sig = Some m 
  1348         \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1349     (is "PROP ?P C") 
  1350   proof (induct ?P C rule: ws_class_induct')
  1351     case Object
  1352     assume "methd G Object sig = Some m" 
  1353     with wf show ?thesis
  1354       by - (rule method_declared_inI, auto) 
  1355   next
  1356     case Subcls
  1357     fix C c
  1358     assume clsC: "class G C = Some c"
  1359     and       m: "methd G C sig = Some m"
  1360     and     hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 
  1361     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1362     show ?thesis
  1363     proof (cases "?newMethods sig")
  1364       case None
  1365       from None ws clsC m hyp 
  1366       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
  1367     next
  1368       case Some
  1369       from Some ws clsC m 
  1370       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
  1371     qed
  1372   qed
  1373 qed
  1374 
  1375 lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
  1376 (assumes methd_C: "methd G C sig = Some m" and
  1377                     ws: "ws_prog G" and
  1378                   clsC: "class G C = Some c" and
  1379              neq_C_Obj: "C\<noteq>Object" )  
  1380 "\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
  1381   \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
  1382  \<rbrakk> \<Longrightarrow> P"
  1383 proof -
  1384   let ?inherited   = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 
  1385                               (methd G (super c))"
  1386   let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1387   from ws clsC neq_C_Obj methd_C 
  1388   have methd_unfold: "(?inherited ++ ?new) sig = Some m"
  1389     by (simp add: methd_rec)
  1390   assume NewMethod: "?new sig = Some m \<Longrightarrow> P"
  1391   assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); 
  1392                             methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P"
  1393   show P
  1394   proof (cases "?new sig")
  1395     case None
  1396     with methd_unfold have "?inherited sig = Some m"
  1397       by (auto)
  1398     with InheritedMethod show P by blast
  1399   next
  1400     case Some
  1401     with methd_unfold have "?new sig = Some m"
  1402       by auto
  1403     with NewMethod show P by blast
  1404   qed
  1405 qed
  1406 
  1407   
  1408 lemma methd_member_of:
  1409  (assumes wf: "wf_prog G") 
  1410   "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
  1411   (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
  1412 proof -
  1413   from wf   have   ws: "ws_prog G" ..
  1414   assume defC: "is_class G C"
  1415   from defC ws 
  1416   show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
  1417   proof (induct rule: ws_class_induct')  
  1418     case Object
  1419     with wf have declC: "declclass m = Object"
  1420       by (blast intro: declclass_methd_Object)
  1421     with Object wf have "G\<turnstile>Methd sig m declared_in Object"
  1422       by (auto dest: methd_declaredD simp del: methd_Object)
  1423     with declC 
  1424     show "?MemberOf Object"
  1425       by (auto intro!: members.Immediate
  1426                   simp del: methd_Object)
  1427   next
  1428     case (Subcls C c)
  1429     assume  clsC: "class G C = Some c" and
  1430        neq_C_Obj: "C \<noteq> Object"  
  1431     assume methd: "?Method C"
  1432     from methd ws clsC neq_C_Obj
  1433     show "?MemberOf C"
  1434     proof (cases rule: methd_rec_Some_cases)
  1435       case NewMethod
  1436       with clsC show ?thesis
  1437 	by (auto dest: method_declared_inI intro!: members.Immediate)
  1438     next
  1439       case InheritedMethod
  1440       then show "?thesis"
  1441 	by (blast dest: inherits_member)
  1442     qed
  1443   qed
  1444 qed
  1445 
  1446 lemma current_methd: 
  1447       "\<lbrakk>table_of (methods c) sig = Some new;
  1448         ws_prog G; class G C = Some c; C \<noteq> Object; 
  1449         methd G (super c) sig = Some old\<rbrakk> 
  1450     \<Longrightarrow> methd G C sig = Some (C,new)"
  1451 by (auto simp add: methd_rec
  1452             intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
  1453 
  1454 lemma wf_prog_staticD:
  1455  (assumes     wf: "wf_prog G" and 
  1456             clsC: "class G C = Some c" and
  1457        neq_C_Obj: "C \<noteq> Object" and 
  1458              old: "methd G (super c) sig = Some old" and 
  1459      accmodi_old: "Protected \<le> accmodi old" and
  1460              new: "table_of (methods c) sig = Some new"
  1461  ) "is_static new = is_static old"
  1462 proof -
  1463   from clsC wf 
  1464   have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
  1465   from wf clsC neq_C_Obj
  1466   have is_cls_super: "is_class G (super c)" 
  1467     by (blast dest: wf_prog_acc_superD is_acc_classD)
  1468   from wf is_cls_super old 
  1469   have old_member_of: "G\<turnstile>Methd sig old member_of (super c)"  
  1470     by (rule methd_member_of)
  1471   from old wf is_cls_super 
  1472   have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)"
  1473     by (auto dest: methd_declared_in_declclass)
  1474   from new clsC 
  1475   have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C"
  1476     by (auto intro: method_declared_inI)
  1477   note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
  1478   from clsC neq_C_Obj
  1479   have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1480     by (rule subcls1I)
  1481   then have "G\<turnstile>C \<prec>\<^sub>C super c" ..
  1482   also from old wf is_cls_super
  1483   have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC)
  1484   finally have subcls_C_old:  "G\<turnstile>C \<prec>\<^sub>C (declclass old)" .
  1485   from accmodi_old 
  1486   have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C"
  1487     by (auto simp add: inheritable_in_def
  1488                  dest: acc_modi_le_Dests)
  1489   show ?thesis
  1490   proof (cases "is_static new")
  1491     case True
  1492     with subcls_C_old new_declared old_declared inheritable
  1493     have "G,sig\<turnstile>(C,new) hides old"
  1494       by (auto intro: hidesI)
  1495     with True wf_cdecl neq_C_Obj new 
  1496     show ?thesis
  1497       by (auto dest: wf_cdecl_hides_SomeD)
  1498   next
  1499     case False
  1500     with subcls_C_old new_declared old_declared inheritable subcls1_C_super
  1501          old_member_of
  1502     have "G,sig\<turnstile>(C,new) overrides\<^sub>S old"
  1503       by (auto intro: stat_overridesR.Direct)
  1504     with False wf_cdecl neq_C_Obj new 
  1505     show ?thesis
  1506       by (auto dest: wf_cdecl_overrides_SomeD)
  1507   qed
  1508 qed
  1509 
  1510 lemma inheritable_instance_methd: 
  1511  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1512               is_cls_D: "is_class G D" and
  1513                     wf: "wf_prog G" and 
  1514                    old: "methd G D sig = Some old" and
  1515            accmodi_old: "Protected \<le> accmodi old" and  
  1516         not_static_old: "\<not> is_static old"
  1517  )  
  1518   "\<exists>new. methd G C sig = Some new \<and>
  1519          (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
  1520  (is "(\<exists>new. (?Constraint C new old))")
  1521 proof -
  1522   from subclseq_C_D is_cls_D 
  1523   have is_cls_C: "is_class G C" by (rule subcls_is_class2) 
  1524   from wf 
  1525   have ws: "ws_prog G" ..
  1526   from is_cls_C ws subclseq_C_D 
  1527   show "\<exists>new. ?Constraint C new old"
  1528   proof (induct rule: ws_class_induct')
  1529     case (Object co)
  1530     then have eq_D_Obj: "D=Object" by auto
  1531     with old 
  1532     have "?Constraint Object old old"
  1533       by auto
  1534     with eq_D_Obj 
  1535     show "\<exists> new. ?Constraint Object new old" by auto
  1536   next
  1537     case (Subcls C c)
  1538     assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old"
  1539     assume clsC: "class G C = Some c"
  1540     assume neq_C_Obj: "C\<noteq>Object"
  1541     from clsC wf 
  1542     have wf_cdecl: "wf_cdecl G (C,c)" 
  1543       by (rule wf_prog_cdecl)
  1544     from ws clsC neq_C_Obj
  1545     have is_cls_super: "is_class G (super c)"
  1546       by (auto dest: ws_prog_cdeclD)
  1547     from clsC wf neq_C_Obj 
  1548     have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and
  1549 	 subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1550       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
  1551               intro: subcls1I)
  1552     show "\<exists>new. ?Constraint C new old"
  1553     proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D")
  1554       case False
  1555       from False Subcls 
  1556       have eq_C_D: "C=D"
  1557 	by (auto dest: subclseq_superD)
  1558       with old 
  1559       have "?Constraint C old old"
  1560 	by auto
  1561       with eq_C_D 
  1562       show "\<exists> new. ?Constraint C new old" by auto
  1563     next
  1564       case True
  1565       with hyp obtain super_method
  1566 	where super: "?Constraint (super c) super_method old" by blast
  1567       from super not_static_old
  1568       have not_static_super: "\<not> is_static super_method"
  1569 	by (auto dest!: stat_overrides_commonD)
  1570       from super old wf accmodi_old
  1571       have accmodi_super_method: "Protected \<le> accmodi super_method"
  1572 	by (auto dest!: wf_prog_stat_overridesD
  1573                  intro: order_trans)
  1574       from super accmodi_old wf
  1575       have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
  1576 	by (auto dest!: wf_prog_stat_overridesD
  1577                         acc_modi_le_Dests
  1578               simp add: inheritable_in_def)	           
  1579       from super wf is_cls_super
  1580       have member: "G\<turnstile>Methd sig super_method member_of (super c)"
  1581 	by (auto intro: methd_member_of) 
  1582       from member
  1583       have decl_super_method:
  1584         "G\<turnstile>Methd sig super_method declared_in (declclass super_method)"
  1585 	by (auto dest: member_of_declC)
  1586       from super subcls1_C_super ws is_cls_super 
  1587       have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)"
  1588 	by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 
  1589       show "\<exists> new. ?Constraint C new old"
  1590       proof (cases "methd G C sig")
  1591 	case None
  1592 	have "methd G (super c) sig = None"
  1593 	proof -
  1594 	  from clsC ws None 
  1595 	  have no_new: "table_of (methods c) sig = None" 
  1596 	    by (auto simp add: methd_rec)
  1597 	  with clsC 
  1598 	  have undeclared: "G\<turnstile>mid sig undeclared_in C"
  1599 	    by (auto simp add: undeclared_in_def cdeclaredmethd_def)
  1600 	  with inheritable member superAccessible subcls1_C_super
  1601 	  have inherits: "G\<turnstile>C inherits (method sig super_method)"
  1602 	    by (auto simp add: inherits_def)
  1603 	  with clsC ws no_new super neq_C_Obj
  1604 	  have "methd G C sig = Some super_method"
  1605 	    by (auto simp add: methd_rec override_def
  1606 	                intro: filter_tab_SomeI)
  1607           with None show ?thesis
  1608 	    by simp
  1609 	qed
  1610 	with super show ?thesis by auto
  1611       next
  1612 	case (Some new)
  1613 	from this ws clsC neq_C_Obj
  1614 	show ?thesis
  1615 	proof (cases rule: methd_rec_Some_cases)
  1616 	  case InheritedMethod
  1617 	  with super Some show ?thesis 
  1618 	    by auto
  1619 	next
  1620 	  case NewMethod
  1621 	  assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig 
  1622                        = Some new"
  1623 	  from new 
  1624 	  have declcls_new: "declclass new = C" 
  1625 	    by auto
  1626 	  from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
  1627 	  have not_static_new: "\<not> is_static new" 
  1628 	    by (auto dest: wf_prog_staticD) 
  1629 	  from clsC new
  1630 	  have decl_new: "G\<turnstile>Methd sig new declared_in C"
  1631 	    by (auto simp add: declared_in_def cdeclaredmethd_def)
  1632 	  from not_static_new decl_new decl_super_method
  1633 	       member subcls1_C_super inheritable declcls_new subcls_C_super 
  1634 	  have "G,sig\<turnstile> new overrides\<^sub>S super_method"
  1635 	    by (auto intro: stat_overridesR.Direct) 
  1636 	  with super Some
  1637 	  show ?thesis
  1638 	    by (auto intro: stat_overridesR.Indirect)
  1639 	qed
  1640       qed
  1641     qed
  1642   qed
  1643 qed
  1644 
  1645 lemma inheritable_instance_methd_cases [consumes 6
  1646                                        , case_names Inheritance Overriding]: 
  1647  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1648               is_cls_D: "is_class G D" and
  1649                     wf: "wf_prog G" and 
  1650                    old: "methd G D sig = Some old" and
  1651            accmodi_old: "Protected \<le> accmodi old" and  
  1652         not_static_old: "\<not> is_static old" and
  1653            inheritance:  "methd G C sig = Some old \<Longrightarrow> P" and
  1654             overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
  1655                                    G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
  1656         
  1657  ) "P"
  1658 proof -
  1659 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1660 show ?thesis
  1661   by (auto dest: inheritable_instance_methd intro: inheritance overriding)
  1662 qed
  1663 
  1664 lemma inheritable_instance_methd_props: 
  1665  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1666               is_cls_D: "is_class G D" and
  1667                     wf: "wf_prog G" and 
  1668                    old: "methd G D sig = Some old" and
  1669            accmodi_old: "Protected \<le> accmodi old" and  
  1670         not_static_old: "\<not> is_static old"
  1671  )  
  1672   "\<exists>new. methd G C sig = Some new \<and>
  1673           \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
  1674  (is "(\<exists>new. (?Constraint C new old))")
  1675 proof -
  1676   from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1677   show ?thesis
  1678   proof (cases rule: inheritable_instance_methd_cases)
  1679     case Inheritance
  1680     with not_static_old accmodi_old show ?thesis by auto
  1681   next
  1682     case (Overriding new)
  1683     then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
  1684     with Overriding not_static_old accmodi_old wf 
  1685     show ?thesis 
  1686       by (auto dest!: wf_prog_stat_overridesD
  1687                intro: order_trans)
  1688   qed
  1689 qed
  1690  	  
  1691 (* ### Probleme: Die tollen methd_subcls_cases Lemma wird warscheinlich
  1692   kaum gebraucht: 
  1693 Redundanz: stat_overrides.Direct old declared in declclass old folgt aus
  1694            member of 
  1695    Problem: Predikate wie overrides, sind global üper die Hierarchie hinweg
  1696             definiert, aber oft barucht man eben zusätlich Induktion
  1697             : von super c auf C; Dann ist aber auss dem Kontext
  1698             die Unterscheidung in die 5 fälle overkill,
  1699             da man dann warscheinlich meistens eh in einem speziellen
  1700             Fall kommt (durch die Hypothesen)
  1701 *)
  1702     
  1703 (* local lemma *)
  1704 ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
  1705 ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
  1706 lemma subint_widen_imethds: 
  1707  "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
  1708   \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
  1709                           accmodi im = accmodi jm \<and>
  1710                           G\<turnstile>resTy im\<preceq>resTy jm"
  1711 proof -
  1712   assume irel: "G\<turnstile>I\<preceq>I J" and
  1713            wf: "wf_prog G" and
  1714      is_iface: "is_iface G J"
  1715   from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
  1716                (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
  1717   proof (induct ?P I rule: converse_rtrancl_induct) 
  1718     case Id
  1719     assume "jm \<in> imethds G J sig"
  1720     then show "?Concl J" by  (blast elim: bexI')
  1721   next
  1722     case Step
  1723     fix I SI
  1724     assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
  1725             subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
  1726                     hyp: "PROP ?P SI" and
  1727                      jm: "jm \<in> imethds G J sig"
  1728     from subint1_I_SI 
  1729     obtain i where
  1730       ifI: "iface G I = Some i" and
  1731        SI: "SI \<in> set (isuperIfs i)"
  1732       by (blast dest: subint1D)
  1733 
  1734     let ?newMethods 
  1735           = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
  1736     show "?Concl I"
  1737     proof (cases "?newMethods sig = {}")
  1738       case True
  1739       with ifI SI hyp wf jm 
  1740       show "?thesis" 
  1741 	by (auto simp add: imethds_rec) 
  1742     next
  1743       case False
  1744       from ifI wf False
  1745       have imethds: "imethds G I sig = ?newMethods sig"
  1746 	by (simp add: imethds_rec)
  1747       from False
  1748       obtain im where
  1749         imdef: "im \<in> ?newMethods sig" 
  1750 	by (blast)
  1751       with imethds 
  1752       have im: "im \<in> imethds G I sig"
  1753 	by (blast)
  1754       with im wf ifI 
  1755       obtain
  1756 	 imStatic: "\<not> is_static im" and
  1757          imPublic: "accmodi im = Public"
  1758 	by (auto dest!: imethds_wf_mhead)	
  1759       from ifI wf 
  1760       have wf_I: "wf_idecl G (I,i)" 
  1761 	by (rule wf_prog_idecl)
  1762       with SI wf  
  1763       obtain si where
  1764 	 ifSI: "iface G SI = Some si" and
  1765 	wf_SI: "wf_idecl G (SI,si)" 
  1766 	by (auto dest!: wf_idecl_supD is_acc_ifaceD
  1767                   dest: wf_prog_idecl)
  1768       from jm hyp 
  1769       obtain sim::"qtname \<times> mhead"  where
  1770                       sim: "sim \<in> imethds G SI sig" and
  1771          eq_static_sim_jm: "is_static sim = is_static jm" and 
  1772          eq_access_sim_jm: "accmodi sim = accmodi jm" and 
  1773         resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm"
  1774 	by blast
  1775       with wf_I SI imdef sim 
  1776       have "G\<turnstile>resTy im\<preceq>resTy sim"   
  1777 	by (auto dest!: wf_idecl_hidings hidings_entailsD)
  1778       with wf resTy_widen_sim_jm 
  1779       have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm"
  1780 	by (blast intro: widen_trans)
  1781       from sim wf ifSI  
  1782       obtain
  1783 	simStatic: "\<not> is_static sim" and
  1784         simPublic: "accmodi sim = Public"
  1785 	by (auto dest!: imethds_wf_mhead)
  1786       from im 
  1787            imStatic simStatic eq_static_sim_jm
  1788            imPublic simPublic eq_access_sim_jm
  1789            resTy_widen_im_jm
  1790       show ?thesis 
  1791 	by auto 
  1792     qed
  1793   qed
  1794 qed
  1795      
  1796 (* Tactical version *)
  1797 (* 
  1798 lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow>  
  1799   \<forall> jm \<in> imethds G J sig.  
  1800   \<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> 
  1801                           access (mthd im)= access (mthd jm) \<and>
  1802                           G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)"
  1803 apply (erule converse_rtrancl_induct)
  1804 apply  (clarsimp elim!: bexI')
  1805 apply (frule subint1D)
  1806 apply clarify
  1807 apply (erule ballE')
  1808 apply  fast
  1809 apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl)
  1810 apply clarsimp
  1811 apply (subst imethds_rec, assumption, erule wf_ws_prog)
  1812 apply (unfold overrides_t_def)
  1813 apply (drule (1) wf_prog_idecl)
  1814 apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
  1815                                        [THEN is_acc_ifaceD [THEN conjunct1]]]])
  1816 apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
  1817                   sig ={}")
  1818 apply   force
  1819 
  1820 apply   (simp only:)
  1821 apply   (simp)
  1822 apply   clarify
  1823 apply   (frule wf_idecl_hidings [THEN hidings_entailsD])
  1824 apply     blast
  1825 apply     blast
  1826 apply   (rule bexI')
  1827 apply     simp
  1828 apply     (drule table_of_map_SomeI [of _ "sig"])
  1829 apply     simp
  1830 
  1831 apply     (frule wf_idecl_mhead [of _ _ _ "sig"])
  1832 apply       (rule table_of_Some_in_set)
  1833 apply       assumption
  1834 apply     auto
  1835 done
  1836 *)
  1837     
  1838 
  1839 (* local lemma *)
  1840 lemma implmt1_methd: 
  1841  "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow>  
  1842   \<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> 
  1843                        G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1844                        accmodi im = Public \<and> accmodi cm = Public"
  1845 apply (drule implmt1D)
  1846 apply clarify
  1847 apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
  1848 apply (frule (1) imethds_wf_mhead)
  1849 apply  (simp add: is_acc_iface_def)
  1850 apply (force)
  1851 done
  1852 
  1853 
  1854 (* local lemma *)
  1855 lemma implmt_methd [rule_format (no_asm)]: 
  1856 "\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow>  
  1857  (\<forall> im    \<in>imethds G I   sig.  
  1858   \<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> 
  1859                       G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1860                       accmodi im = Public \<and> accmodi cm = Public)"
  1861 apply (frule implmt_is_class)
  1862 apply (erule implmt.induct)
  1863 apply   safe
  1864 apply   (drule (2) implmt1_methd)
  1865 apply   fast
  1866 apply  (drule (1) subint_widen_imethds)
  1867 apply   simp
  1868 apply   assumption
  1869 apply  clarify
  1870 apply  (drule (2) implmt1_methd)
  1871 apply  (force)
  1872 apply (frule subcls1D)
  1873 apply (drule (1) bspec)
  1874 apply clarify
  1875 apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 
  1876                                  OF _ implmt_is_class])
  1877 apply auto 
  1878 done
  1879 
  1880 lemma mheadsD [rule_format (no_asm)]: 
  1881 "emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow>
  1882  (\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> 
  1883           accmethd G S C sig = Some m \<and>
  1884           (declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or>
  1885  (\<exists>I. t = IfaceT I \<and> ((\<exists>im. im  \<in> accimethds G (pid S) I sig \<and> 
  1886           mthd im = mhd emh) \<or> 
  1887   (\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> 
  1888        accmodi m \<noteq> Private \<and> 
  1889        declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or>
  1890  (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
  1891         accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 
  1892         declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
  1893 apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1])
  1894 apply auto
  1895 apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
  1896 apply (auto  dest!: accmethd_SomeD)
  1897 done
  1898 
  1899 lemma mheads_cases [consumes 2, case_names Class_methd 
  1900                     Iface_methd Iface_Object_methd Array_Object_methd]: 
  1901 "\<lbrakk>emh \<in> mheads G S t sig; wf_prog G;
  1902  \<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m;
  1903            (declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh; 
  1904  \<And> I im. \<lbrakk>t = IfaceT I; im  \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk>
  1905           \<Longrightarrow> P emh;
  1906  \<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S);
  1907           accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
  1908          declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh;
  1909  \<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S);
  1910           accmethd G S Object sig = Some m; accmodi m \<noteq> Private; 
  1911           declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow>  P emh 
  1912 \<rbrakk> \<Longrightarrow> P emh"
  1913 by (blast dest!: mheadsD)
  1914 
  1915 lemma declclassD[rule_format]:
  1916  "\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; 
  1917    class G (declclass m) = Some d\<rbrakk>
  1918   \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)"
  1919 proof -
  1920   assume    wf: "wf_prog G"
  1921   then have ws: "ws_prog G" ..
  1922   assume  clsC: "class G C = Some c"
  1923   from clsC ws 
  1924   show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
  1925         \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
  1926          (is "PROP ?P C") 
  1927   proof (induct ?P C rule: ws_class_induct)
  1928     case Object
  1929     fix m d
  1930     assume "methd G Object sig = Some m" 
  1931            "class G (declclass m) = Some d"
  1932     with wf show "?thesis m d" by auto
  1933   next
  1934     case Subcls
  1935     fix C c m d
  1936     assume hyp: "PROP ?P (super c)"
  1937     and      m: "methd G C sig = Some m"
  1938     and  declC: "class G (declclass m) = Some d"
  1939     and   clsC: "class G C = Some c"
  1940     and   nObj: "C \<noteq> Object"
  1941     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
  1942     show "?thesis m d" 
  1943     proof (cases "?newMethods")
  1944       case None
  1945       from None clsC nObj ws m declC hyp  
  1946       show "?thesis" by (auto simp add: methd_rec)
  1947     next
  1948       case Some
  1949       from Some clsC nObj ws m declC hyp  
  1950       show "?thesis" 
  1951 	by (auto simp add: methd_rec
  1952                      dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1953     qed
  1954   qed
  1955 qed
  1956 
  1957 (* Tactical version *)
  1958 (*
  1959 lemma declclassD[rule_format]:
  1960  "wf_prog G \<longrightarrow>  
  1961  (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
  1962   class G (declclass m) = Some d
  1963  \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
  1964 apply (rule class_rec.induct)
  1965 apply (rule impI)
  1966 apply (rule allI)+
  1967 apply (rule impI)
  1968 apply (case_tac "C=Object")
  1969 apply   (force simp add: methd_rec)
  1970 
  1971 apply   (subst methd_rec)
  1972 apply     (blast dest: wf_ws_prog)+
  1973 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
  1974 apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1975 done
  1976 *)
  1977 
  1978 lemma dynmethd_Object:
  1979  (assumes statM: "methd G Object sig = Some statM" and
  1980         private: "accmodi statM = Private" and 
  1981        is_cls_C: "is_class G C" and
  1982              wf: "wf_prog G"
  1983  ) "dynmethd G Object C sig = Some statM"
  1984 proof -
  1985   from is_cls_C wf 
  1986   have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
  1987     by (auto intro: subcls_ObjectI)
  1988   from wf have ws: "ws_prog G" 
  1989     by simp
  1990   from wf 
  1991   have is_cls_Obj: "is_class G Object" 
  1992     by simp
  1993   from statM subclseq is_cls_Obj ws private
  1994   show ?thesis
  1995   proof (cases rule: dynmethd_cases)
  1996     case Static then show ?thesis .
  1997   next
  1998     case Overrides 
  1999     with private show ?thesis 
  2000       by (auto dest: no_Private_override)
  2001   qed
  2002 qed
  2003 
  2004 lemma wf_imethds_hiding_objmethdsD: 
  2005   (assumes     old: "methd G Object sig = Some old" and
  2006            is_if_I: "is_iface G I" and
  2007                 wf: "wf_prog G" and    
  2008        not_private: "accmodi old \<noteq> Private" and
  2009                new: "new \<in> imethds G I sig" 
  2010   ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
  2011 proof -
  2012   from wf have ws: "ws_prog G" by simp
  2013   {
  2014     fix I i new
  2015     assume ifI: "iface G I = Some i"
  2016     assume new: "table_of (imethods i) sig = Some new" 
  2017     from ifI new not_private wf old  
  2018     have "?P (I,new)"
  2019       by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
  2020             simp del: methd_Object)
  2021   } note hyp_newmethod = this  
  2022   from is_if_I ws new 
  2023   show ?thesis
  2024   proof (induct rule: ws_interface_induct)
  2025     case (Step I i)
  2026     assume ifI: "iface G I = Some i" 
  2027     assume new: "new \<in> imethds G I sig" 
  2028     from Step
  2029     have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)"
  2030       by auto 
  2031     from new ifI ws
  2032     show "?P new"
  2033     proof (cases rule: imethds_cases)
  2034       case NewMethod
  2035       with ifI hyp_newmethod
  2036       show ?thesis
  2037 	by auto
  2038     next
  2039       case (InheritedMethod J)
  2040       assume "J \<in> set (isuperIfs i)" 
  2041              "new \<in> imethds G J sig"
  2042       with hyp 
  2043       show "?thesis"
  2044 	by auto
  2045     qed
  2046   qed
  2047 qed
  2048 
  2049 text {*
  2050 Which dynamic classes are valid to look up a member of a distinct static type?
  2051 We have to distinct class members (named static members in Java) 
  2052 from instance members. Class members are global to all Objects of a class,
  2053 instance members are local to a single Object instance. If a member is
  2054 equipped with the static modifier it is a class member, else it is an 
  2055 instance member.
  2056 The following table gives an overview of the current framework. We assume
  2057 to have a reference with static type statT and a dynamic class dynC. Between
  2058 both of these types the widening relation holds 
  2059 @{term "G\<turnstile>Class dynC\<preceq> statT"}. Unfortunately this ordinary widening relation 
  2060 isn't enough to describe the valid lookup classes, since we must cope the
  2061 special cases of arrays and interfaces,too. If we statically expect an array or
  2062 inteface we may lookup a field or a method in Object which isn't covered in 
  2063 the widening relation.
  2064 
  2065 statT      field         instance method       static (class) method
  2066 ------------------------------------------------------------------------
  2067  NullT      /                  /                   /
  2068  Iface      /                dynC                Object
  2069  Class    dynC               dynC                 dynC
  2070  Array      /                Object              Object
  2071 
  2072 In most cases we con lookup the member in the dynamic class. But as an
  2073 interface can't declare new static methods, nor an array can define new
  2074 methods at all, we have to lookup methods in the base class Object.
  2075 
  2076 The limitation to classes in the field column is artificial  and comes out
  2077 of the typing rule for the field access (see rule @{text "FVar"} in the 
  2078 welltyping relation @{term "wt"} in theory WellType). 
  2079 I stems out of the fact, that Object
  2080 indeed has no non private fields. So interfaces and arrays can actually
  2081 have no fields at all and a field access would be senseless. (In Java
  2082 interfaces are allowed to declare new fields but in current Bali not!).
  2083 So there is no principal reason why we should not allow Objects to declare
  2084 non private fields. Then we would get the following column:
  2085        
  2086  statT    field
  2087 ----------------- 
  2088  NullT      /  
  2089  Iface    Object 
  2090  Class    dynC 
  2091  Array    Object
  2092 *}
  2093 consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  2094                         ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
  2095 primrec
  2096 "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  2097 "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  2098               = (if static_membr 
  2099                     then dynC=Object 
  2100                     else G\<turnstile>Class dynC\<preceq> Iface I)"
  2101 "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  2102 "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  2103 
  2104 lemma valid_lookup_cls_is_class:
  2105  (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
  2106       ty_statT: "isrtype G statT" and
  2107             wf: "wf_prog G"
  2108  ) "is_class G dynC"
  2109 proof (cases statT)
  2110   case NullT
  2111   with dynC ty_statT show ?thesis
  2112     by (auto dest: widen_NT2)
  2113 next
  2114   case (IfaceT I)
  2115   with dynC wf show ?thesis
  2116     by (auto dest: implmt_is_class)
  2117 next
  2118   case (ClassT C)
  2119   with dynC ty_statT show ?thesis
  2120     by (auto dest: subcls_is_class2)
  2121 next
  2122   case (ArrayT T)
  2123   with dynC wf show ?thesis
  2124     by (auto)
  2125 qed
  2126 
  2127 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2128 ML_setup {*
  2129 simpset_ref() := simpset() delloop "split_all_tac";
  2130 claset_ref () := claset () delSWrapper "split_all_tac"
  2131 *}
  2132 lemma dynamic_mheadsD:   
  2133 "\<lbrakk>emh \<in> mheads G S statT sig;    
  2134   G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
  2135   isrtype G statT; wf_prog G
  2136  \<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: 
  2137           is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh"
  2138 proof - 
  2139   assume      emh: "emh \<in> mheads G S statT sig"
  2140   and          wf: "wf_prog G"
  2141   and   dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)"
  2142   and      istype: "isrtype G statT"
  2143   from dynC_Prop istype wf 
  2144   obtain y where
  2145     dynC: "class G dynC = Some y" 
  2146     by (auto dest: valid_lookup_cls_is_class)
  2147   from emh wf show ?thesis
  2148   proof (cases rule: mheads_cases)
  2149     case Class_methd
  2150     fix statC statDeclC sm
  2151     assume     statC: "statT = ClassT statC"
  2152     assume            "accmethd G S statC sig = Some sm"
  2153     then have     sm: "methd G statC sig = Some sm" 
  2154       by (blast dest: accmethd_SomeD)  
  2155     assume eq_mheads: "mhead (mthd sm) = mhd emh"
  2156     from statC 
  2157     have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
  2158       by (simp add: dynlookup_def)
  2159     from wf statC istype dynC_Prop sm 
  2160     obtain dm where
  2161       "dynmethd G statC dynC sig = Some dm"
  2162       "is_static dm = is_static sm" 
  2163       "G\<turnstile>resTy dm\<preceq>resTy sm"  
  2164       by (force dest!: ws_dynmethd accmethd_SomeD)
  2165     with dynlookup eq_mheads 
  2166     show ?thesis 
  2167       by (cases emh type: *) (auto)
  2168   next
  2169     case Iface_methd
  2170     fix I im
  2171     assume    statI: "statT = IfaceT I" and
  2172           eq_mheads: "mthd im = mhd emh" and
  2173                      "im \<in> accimethds G (pid S) I sig" 
  2174     then have im: "im \<in> imethds G I sig" 
  2175       by (blast dest: accimethdsD)
  2176     with istype statI eq_mheads wf 
  2177     have not_static_emh: "\<not> is_static emh"
  2178       by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2179     from statI im
  2180     have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2181       by (auto simp add: dynlookup_def dynimethd_def) 
  2182     from wf dynC_Prop statI istype im not_static_emh 
  2183     obtain dm where
  2184       "methd G dynC sig = Some dm"
  2185       "is_static dm = is_static im" 
  2186       "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2187       by (force dest: implmt_methd)
  2188     with dynlookup eq_mheads
  2189     show ?thesis 
  2190       by (cases emh type: *) (auto)
  2191   next
  2192     case Iface_Object_methd
  2193     fix I sm
  2194     assume   statI: "statT = IfaceT I" and
  2195                 sm: "accmethd G S Object sig = Some sm" and 
  2196          eq_mheads: "mhead (mthd sm) = mhd emh" and
  2197              nPriv: "accmodi sm \<noteq> Private"
  2198      show ?thesis 
  2199      proof (cases "imethds G I sig = {}")
  2200        case True
  2201        with statI 
  2202        have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig"
  2203 	 by (simp add: dynlookup_def dynimethd_def)
  2204        from wf dynC 
  2205        have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2206 	 by (auto intro: subcls_ObjectI)
  2207        from wf dynC dynC_Prop istype sm subclsObj 
  2208        obtain dm where
  2209 	 "dynmethd G Object dynC sig = Some dm"
  2210 	 "is_static dm = is_static sm" 
  2211 	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)"  
  2212 	 by (auto dest!: ws_dynmethd accmethd_SomeD 
  2213                   intro: class_Object [OF wf] intro: that)
  2214        with dynlookup eq_mheads
  2215        show ?thesis 
  2216 	 by (cases emh type: *) (auto)
  2217      next
  2218        case False
  2219        with statI
  2220        have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2221 	 by (simp add: dynlookup_def dynimethd_def)
  2222        from istype statI
  2223        have "is_iface G I"
  2224 	 by auto
  2225        with wf sm nPriv False 
  2226        obtain im where
  2227 	      im: "im \<in> imethds G I sig" and
  2228 	 eq_stat: "is_static im = is_static sm" and
  2229          resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)"
  2230 	 by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD)
  2231        from im wf statI istype eq_stat eq_mheads
  2232        have not_static_sm: "\<not> is_static emh"
  2233 	 by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2234        from im wf dynC_Prop dynC istype statI not_static_sm
  2235        obtain dm where
  2236 	 "methd G dynC sig = Some dm"
  2237 	 "is_static dm = is_static im" 
  2238 	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2239 	 by (auto dest: implmt_methd)
  2240        with wf eq_stat resProp dynlookup eq_mheads
  2241        show ?thesis 
  2242 	 by (cases emh type: *) (auto intro: widen_trans)
  2243      qed
  2244   next
  2245     case Array_Object_methd
  2246     fix T sm
  2247     assume statArr: "statT = ArrayT T" and
  2248                 sm: "accmethd G S Object sig = Some sm" and 
  2249          eq_mheads: "mhead (mthd sm) = mhd emh" 
  2250     from statArr dynC_Prop wf
  2251     have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
  2252       by (auto simp add: dynlookup_def dynmethd_C_C)
  2253     with sm eq_mheads sm 
  2254     show ?thesis 
  2255       by (cases emh type: *) (auto dest: accmethd_SomeD)
  2256   qed
  2257 qed
  2258 declare split_paired_All [simp] split_paired_Ex [simp]
  2259 ML_setup {*
  2260 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  2261 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  2262 *}
  2263 
  2264 (* Tactical version *)
  2265 (*
  2266 lemma dynamic_mheadsD: "  
  2267  \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y;  
  2268    if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; 
  2269    isrtype G statT\<rbrakk> \<Longrightarrow>  
  2270   \<exists>m \<in> dynlookup G statT dynC sig: 
  2271      static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)"
  2272 apply (drule mheadsD)
  2273 apply safe
  2274        -- reftype statT is a class  
  2275 apply  (case_tac "\<exists>T. ClassT C = ArrayT T")
  2276 apply    (simp)
  2277 
  2278 apply    (clarsimp simp add: dynlookup_def )
  2279 apply    (frule_tac statC="C" and dynC="dynC"  and sig="sig"  
  2280          in ws_dynmethd)
  2281 apply      assumption+
  2282 apply    (case_tac "emh")  
  2283 apply    (force dest: accmethd_SomeD)
  2284 
  2285        -- reftype statT is a interface, method defined in interface 
  2286 apply    (clarsimp simp add: dynlookup_def)
  2287 apply    (drule (1) implmt_methd)
  2288 apply      blast
  2289 apply      blast
  2290 apply    (clarify)  
  2291 apply    (unfold dynimethd_def)
  2292 apply    (rule_tac x="cm" in bexI)
  2293 apply      (case_tac "emh")
  2294 apply      force
  2295 
  2296 apply      force
  2297 
  2298         -- reftype statT is a interface, method defined in Object 
  2299 apply    (simp add: dynlookup_def)
  2300 apply    (simp only: dynimethd_def)
  2301 apply    (case_tac "imethds G I sig = {}")
  2302 apply       simp
  2303 apply       (frule_tac statC="Object" and dynC="dynC"  and sig="sig"  
  2304              in ws_dynmethd)
  2305 apply          (blast intro: subcls_ObjectI wf_ws_prog) 
  2306 apply          (blast dest: class_Object)
  2307 apply       (case_tac "emh") 
  2308 apply       (force dest: accmethd_SomeD)
  2309 
  2310 apply       simp
  2311 apply       (subgoal_tac "\<exists> im. im \<in> imethds G I sig") 
  2312 prefer 2      apply blast
  2313 apply       clarify
  2314 apply       (frule (1) implmt_methd)
  2315 apply         simp
  2316 apply         blast  
  2317 apply       (clarify dest!: accmethd_SomeD)
  2318 apply       (frule (4) iface_overrides_Object)
  2319 apply       clarify
  2320 apply       (case_tac emh)
  2321 apply       force
  2322 
  2323         -- reftype statT is a array
  2324 apply    (simp add: dynlookup_def)
  2325 apply    (case_tac emh)
  2326 apply    (force dest: accmethd_SomeD simp add: dynmethd_def)
  2327 done
  2328 *)
  2329 
  2330 (* FIXME occasionally convert to ws_class_induct*) 
  2331 lemma methd_declclass:
  2332 "\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> 
  2333  \<Longrightarrow> methd G (declclass m) sig = Some m"
  2334 proof -
  2335   assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m"
  2336   have "wf_prog G  \<longrightarrow> 
  2337 	   (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
  2338                    \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
  2339   proof (rule class_rec.induct,intro allI impI)
  2340     fix G C c m
  2341     assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
  2342                      ?P G (super c)"
  2343     assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  2344             m: "methd G C sig = Some m"
  2345     show "methd G (declclass m) sig = Some m"
  2346     proof (cases "C=Object")
  2347       case True
  2348       with wf m show ?thesis by (auto intro: table_of_map_SomeI)
  2349     next
  2350       let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  2351       let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  2352       case False
  2353       with cls_C wf m
  2354       have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  2355 	by (simp add: methd_rec)
  2356       show ?thesis
  2357       proof (cases "?table sig")
  2358 	case None
  2359 	from this methd_C have "?filter (methd G (super c)) sig = Some m"
  2360 	  by simp
  2361 	moreover
  2362 	from wf cls_C False obtain sup where "class G (super c) = Some sup"
  2363 	  by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  2364 	moreover note wf False cls_C 
  2365 	ultimately show ?thesis by (auto intro: hyp [rule_format])
  2366       next
  2367 	case Some
  2368 	from this methd_C m show ?thesis by auto 
  2369       qed
  2370     qed
  2371   qed	
  2372   with asm show ?thesis by auto
  2373 qed
  2374 
  2375 lemma dynmethd_declclass:
  2376  "\<lbrakk>dynmethd G statC dynC sig = Some m;
  2377    wf_prog G; is_class G statC
  2378   \<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m"
  2379 by (auto dest: dynmethd_declC)
  2380 
  2381 lemma dynlookup_declC:
  2382  "\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G;
  2383    is_class G dynC;isrtype G statT
  2384   \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)"
  2385 by (cases "statT")
  2386    (auto simp add: dynlookup_def dynimethd_def 
  2387              dest: methd_declC dynmethd_declC)
  2388 
  2389 lemma dynlookup_Array_declclassD [simp]:
  2390 "\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> 
  2391  \<Longrightarrow> declclass dm = Object"
  2392 proof -
  2393   assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm"
  2394   assume wf: "wf_prog G"
  2395   from wf have ws: "ws_prog G" by auto
  2396   from wf have is_cls_Obj: "is_class G Object" by auto
  2397   from dynL wf
  2398   show ?thesis
  2399     by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws]
  2400                  dest: methd_Object_SomeD)
  2401 qed   
  2402   
  2403 
  2404 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2405 ML_setup {*
  2406 simpset_ref() := simpset() delloop "split_all_tac";
  2407 claset_ref () := claset () delSWrapper "split_all_tac"
  2408 *}
  2409 lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
  2410   dt=empty_dt \<longrightarrow> (case T of 
  2411                      Inl T \<Rightarrow> is_type (prg E) T 
  2412                    | Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))"
  2413 apply (unfold empty_dt_def)
  2414 apply (erule wt.induct)
  2415 apply (auto split del: split_if_asm simp del: snd_conv 
  2416             simp add: is_acc_class_def is_acc_type_def)
  2417 apply    (erule typeof_empty_is_type)
  2418 apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1, 
  2419         force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
  2420 apply  (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
  2421 apply  (drule_tac [2] accfield_fields) 
  2422 apply  (frule class_Object)
  2423 apply  (auto dest: accmethd_rT_is_type 
  2424                    imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type]
  2425              dest!:accimethdsD
  2426              simp del: class_Object
  2427              simp add: is_acc_type_def
  2428     )
  2429 done
  2430 declare split_paired_All [simp] split_paired_Ex [simp]
  2431 ML_setup {*
  2432 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  2433 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  2434 *}
  2435 
  2436 lemma ty_expr_is_type: 
  2437 "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2438 by (auto dest!: wt_is_type)
  2439 lemma ty_var_is_type: 
  2440 "\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2441 by (auto dest!: wt_is_type)
  2442 lemma ty_exprs_is_type: 
  2443 "\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))"
  2444 by (auto dest!: wt_is_type)
  2445 
  2446 
  2447 lemma static_mheadsD: 
  2448  "\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; 
  2449    invmode (mhd emh) e \<noteq> IntVir 
  2450   \<rbrakk> \<Longrightarrow> \<exists>m. (   (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m)
  2451                \<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> 
  2452           declrefT emh = ClassT (declclass m) \<and>  mhead (mthd m) = (mhd emh)"
  2453 apply (subgoal_tac "is_static emh \<or> e = Super")
  2454 defer apply (force simp add: invmode_def)
  2455 apply (frule  ty_expr_is_type)
  2456 apply   simp
  2457 apply (case_tac "is_static emh")
  2458 apply  (frule (1) mheadsD)
  2459 apply  clarsimp
  2460 apply  safe
  2461 apply    blast
  2462 apply   (auto dest!: imethds_wf_mhead
  2463                      accmethd_SomeD 
  2464                      accimethdsD
  2465               simp add: accObjectmheads_def Objectmheads_def)
  2466 
  2467 apply  (erule wt_elim_cases)
  2468 apply  (force simp add: cmheads_def)
  2469 done
  2470 
  2471 lemma wt_MethdI:  
  2472 "\<lbrakk>methd G C sig = Some m; wf_prog G;  
  2473   class G C = Some c\<rbrakk> \<Longrightarrow>  
  2474  \<exists>T. \<lparr>prg=G,cls=(declclass m),
  2475       lcl=\<lambda> k. 
  2476           (case k of
  2477              EName e 
  2478              \<Rightarrow> (case e of 
  2479                    VNam v 
  2480                    \<Rightarrow> (table_of (lcls (mbody (mthd m)))
  2481                                 ((pars (mthd m))[\<mapsto>](parTs sig))) v
  2482                  | Res \<Rightarrow> Some (resTy (mthd m)))
  2483            | This \<Rightarrow> if is_static m then None else Some (Class (declclass m)))
  2484      \<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
  2485 apply (frule (2) methd_wf_mdecl, clarify)
  2486 apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
  2487 done
  2488 
  2489 subsection "accessibility concerns"
  2490 
  2491 lemma mheads_type_accessible:
  2492  "\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk>
  2493  \<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)"
  2494 by (erule mheads_cases)
  2495    (auto dest: accmethd_SomeD accessible_from_commonD accimethdsD)
  2496 
  2497 lemma static_to_dynamic_accessible_from_aux:
  2498 "\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> 
  2499  \<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC"
  2500 proof (induct rule: accessible_fromR.induct)
  2501 qed (auto intro: dyn_accessible_fromR.intros 
  2502                  member_of_to_member_in
  2503                  static_to_dynamic_overriding)
  2504 
  2505 lemma static_to_dynamic_accessible_from:
  2506  (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  2507           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2508                 wf: "wf_prog G"
  2509  ) "G\<turnstile>m in dynC dyn_accessible_from accC"
  2510 proof - 
  2511   from stat_acc subclseq 
  2512   show ?thesis (is "?Dyn_accessible m")
  2513   proof (induct rule: accessible_fromR.induct)
  2514     case (Immediate statC m)
  2515     then show "?Dyn_accessible m"
  2516       by (blast intro: dyn_accessible_fromR.Immediate
  2517                        member_inI
  2518                        permits_acc_inheritance)
  2519   next
  2520     case (Overriding _ _ m)
  2521     with wf show "?Dyn_accessible m"
  2522       by (blast intro: dyn_accessible_fromR.Overriding
  2523                        member_inI
  2524                        static_to_dynamic_overriding  
  2525                        rtrancl_trancl_trancl 
  2526                        static_to_dynamic_accessible_from_aux)
  2527   qed
  2528 qed
  2529 
  2530 lemma static_to_dynamic_accessible_from_static:
  2531  (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  2532             static: "is_static m" and
  2533                 wf: "wf_prog G"
  2534  ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
  2535 proof -
  2536   from stat_acc wf 
  2537   have "G\<turnstile>m in statC dyn_accessible_from accC"
  2538     by (auto intro: static_to_dynamic_accessible_from)
  2539   from this static
  2540   show ?thesis
  2541     by (rule dyn_accessible_from_static_declC)
  2542 qed
  2543 
  2544 lemma dynmethd_member_in:
  2545  (assumes    m: "dynmethd G statC dynC sig = Some m" and
  2546    iscls_statC: "is_class G statC" and
  2547             wf: "wf_prog G"
  2548  ) "G\<turnstile>Methd sig m member_in dynC"
  2549 proof -
  2550   from m 
  2551   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2552     by (auto simp add: dynmethd_def)
  2553   from subclseq iscls_statC 
  2554   have iscls_dynC: "is_class G dynC"
  2555     by (rule subcls_is_class2)
  2556   from  iscls_dynC iscls_statC wf m
  2557   have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and>
  2558         methd G (declclass m) sig = Some m" 
  2559     by - (drule dynmethd_declC, auto)
  2560   with wf 
  2561   show ?thesis
  2562     by (auto intro: member_inI dest: methd_member_of)
  2563 qed
  2564 
  2565 lemma dynmethd_access_prop:
  2566   (assumes statM: "methd G statC sig = Some statM" and
  2567         stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
  2568             dynM: "dynmethd G statC dynC sig = Some dynM" and
  2569               wf: "wf_prog G" 
  2570    ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2571 proof -
  2572   from wf have ws: "ws_prog G" ..
  2573   from dynM 
  2574   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2575     by (auto simp add: dynmethd_def)
  2576   from stat_acc 
  2577   have is_cls_statC: "is_class G statC"
  2578     by (auto dest: accessible_from_commonD member_of_is_classD)
  2579   with subclseq 
  2580   have is_cls_dynC: "is_class G dynC"
  2581     by (rule subcls_is_class2)
  2582   from is_cls_statC statM wf 
  2583   have member_statC: "G\<turnstile>Methd sig statM member_of statC"
  2584     by (auto intro: methd_member_of)
  2585   from stat_acc 
  2586   have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)"
  2587     by (auto dest: accessible_from_commonD)
  2588   from statM subclseq is_cls_statC ws 
  2589   show ?thesis
  2590   proof (cases rule: dynmethd_cases)
  2591     case Static
  2592     assume dynmethd: "dynmethd G statC dynC sig = Some statM"
  2593     with dynM have eq_dynM_statM: "dynM=statM" 
  2594       by simp
  2595     with stat_acc subclseq wf 
  2596     show ?thesis
  2597       by (auto intro: static_to_dynamic_accessible_from)
  2598   next
  2599     case (Overrides newM)
  2600     assume dynmethd: "dynmethd G statC dynC sig = Some newM"
  2601     assume override: "G,sig\<turnstile>newM overrides statM"
  2602     assume      neq: "newM\<noteq>statM"
  2603     from dynmethd dynM 
  2604     have eq_dynM_newM: "dynM=newM" 
  2605       by simp
  2606     from dynmethd eq_dynM_newM wf is_cls_statC
  2607     have "G\<turnstile>Methd sig dynM member_in dynC"
  2608       by (auto intro: dynmethd_member_in)
  2609     moreover
  2610     from subclseq
  2611     have "G\<turnstile>dynC\<prec>\<^sub>C statC"
  2612     proof (cases rule: subclseq_cases)
  2613       case Eq
  2614       assume "dynC=statC"
  2615       moreover
  2616       from is_cls_statC obtain c
  2617 	where "class G statC = Some c"
  2618 	by auto
  2619       moreover 
  2620       note statM ws dynmethd 
  2621       ultimately
  2622       have "newM=statM" 
  2623 	by (auto simp add: dynmethd_C_C)
  2624       with neq show ?thesis 
  2625 	by (contradiction)
  2626     next
  2627       case Subcls show ?thesis .
  2628     qed 
  2629     moreover
  2630     from stat_acc wf 
  2631     have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC"
  2632       by (blast intro: static_to_dynamic_accessible_from)
  2633     moreover
  2634     note override eq_dynM_newM
  2635     ultimately show ?thesis
  2636       by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.Overriding)
  2637   qed
  2638 qed
  2639 
  2640 lemma implmt_methd_access:
  2641 (fixes accC::qtname
  2642  assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2643            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2644                isif_I: "is_iface G I" and
  2645                    wf: "wf_prog G" 
  2646  ) "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
  2647             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2648 proof -
  2649   from implements 
  2650   have iscls_dynC: "is_class G dynC" by (rule implmt_is_class)
  2651   from iface_methd
  2652   obtain im
  2653     where "im \<in> imethds G I sig"
  2654     by auto
  2655   with wf implements isif_I 
  2656   obtain dynM 
  2657     where dynM: "methd G dynC sig = Some dynM" and
  2658            pub: "accmodi dynM = Public"
  2659     by (blast dest: implmt_methd)
  2660   with iscls_dynC wf
  2661   have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2662     by (auto intro!: dyn_accessible_fromR.Immediate 
  2663               intro: methd_member_of member_of_to_member_in
  2664                      simp add: permits_acc_def)
  2665   with dynM    
  2666   show ?thesis
  2667     by blast
  2668 qed
  2669 
  2670 corollary implmt_dynimethd_access:
  2671 (fixes accC::qtname
  2672  assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2673            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2674                isif_I: "is_iface G I" and
  2675                    wf: "wf_prog G" 
  2676  ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
  2677             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2678 proof -
  2679   from iface_methd
  2680   have "dynimethd G I dynC sig = methd G dynC sig"
  2681     by (simp add: dynimethd_def)
  2682   with iface_methd implements isif_I wf 
  2683   show ?thesis
  2684     by (simp only:)
  2685        (blast intro: implmt_methd_access)
  2686 qed
  2687 
  2688 lemma dynlookup_access_prop:
  2689  (assumes emh: "emh \<in> mheads G accC statT sig" and
  2690          dynM: "dynlookup G statT dynC sig = Some dynM" and
  2691     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
  2692     isT_statT: "isrtype G statT" and
  2693            wf: "wf_prog G"
  2694  ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2695 proof -
  2696   from emh wf
  2697   have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
  2698     by (rule mheads_type_accessible)
  2699   from dynC_prop isT_statT wf
  2700   have iscls_dynC: "is_class G dynC"
  2701     by (rule valid_lookup_cls_is_class)
  2702   from emh dynC_prop isT_statT wf dynM
  2703   have eq_static: "is_static emh = is_static dynM"
  2704     by (auto dest: dynamic_mheadsD)
  2705   from emh wf show ?thesis
  2706   proof (cases rule: mheads_cases)
  2707     case (Class_methd statC _ statM)
  2708     assume statT: "statT = ClassT statC"
  2709     assume "accmethd G accC statC sig = Some statM"
  2710     then have    statM: "methd G statC sig = Some statM" and
  2711               stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC"
  2712       by (auto dest: accmethd_SomeD)
  2713     from dynM statT
  2714     have dynM': "dynmethd G statC dynC sig = Some dynM"
  2715       by (simp add: dynlookup_def) 
  2716     from statM stat_acc wf dynM'
  2717     show ?thesis
  2718       by (auto dest!: dynmethd_access_prop)
  2719   next
  2720     case (Iface_methd I im)
  2721     then have iface_methd: "imethds G I sig \<noteq> {}" and
  2722                  statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 
  2723       by (auto dest: accimethdsD)
  2724     assume   statT: "statT = IfaceT I"
  2725     assume      im: "im \<in>  accimethds G (pid accC) I sig"
  2726     assume eq_mhds: "mthd im = mhd emh"
  2727     from dynM statT
  2728     have dynM': "dynimethd G I dynC sig = Some dynM"
  2729       by (simp add: dynlookup_def)
  2730     from isT_statT statT 
  2731     have isif_I: "is_iface G I"
  2732       by simp
  2733     show ?thesis
  2734     proof (cases "is_static emh")
  2735       case False
  2736       with statT dynC_prop 
  2737       have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT"
  2738 	by simp
  2739       from statT widen_dynC
  2740       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2741 	by auto    
  2742       from eq_static False 
  2743       have not_static_dynM: "\<not> is_static dynM" 
  2744 	by simp
  2745       from iface_methd implmnt isif_I wf dynM'
  2746       show ?thesis
  2747 	by - (drule implmt_dynimethd_access, auto)
  2748     next
  2749       case True
  2750       assume "is_static emh"
  2751       moreover
  2752       from wf isT_statT statT im 
  2753       have "\<not> is_static im"
  2754 	by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead)
  2755       moreover note eq_mhds
  2756       ultimately show ?thesis
  2757 	by (cases emh) auto
  2758     qed
  2759   next
  2760     case (Iface_Object_methd I statM)
  2761     assume statT: "statT = IfaceT I"
  2762     assume "accmethd G accC Object sig = Some statM"
  2763     then have    statM: "methd G Object sig = Some statM" and
  2764               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2765       by (auto dest: accmethd_SomeD)
  2766     assume not_Private_statM: "accmodi statM \<noteq> Private"
  2767     assume eq_mhds: "mhead (mthd statM) = mhd emh"
  2768     from iscls_dynC wf
  2769     have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2770       by (auto intro: subcls_ObjectI)
  2771     show ?thesis
  2772     proof (cases "imethds G I sig = {}")
  2773       case True
  2774       from dynM statT True
  2775       have dynM': "dynmethd G Object dynC sig = Some dynM"
  2776 	by (simp add: dynlookup_def dynimethd_def)
  2777       from statT  
  2778       have "G\<turnstile>RefT statT \<preceq>Class Object"
  2779 	by auto
  2780       with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT 
  2781         wf dynM' eq_static dynC_prop  
  2782       show ?thesis
  2783 	by - (drule dynmethd_access_prop,force+) 
  2784     next
  2785       case False
  2786       then obtain im where
  2787 	im: "im \<in>  imethds G I sig"
  2788 	by auto
  2789       have not_static_emh: "\<not> is_static emh"
  2790       proof -
  2791 	from im statM statT isT_statT wf not_Private_statM 
  2792 	have "is_static im = is_static statM"
  2793 	  by (auto dest: wf_imethds_hiding_objmethdsD)
  2794 	with wf isT_statT statT im 
  2795 	have "\<not> is_static statM"
  2796 	  by (auto dest: wf_prog_idecl imethds_wf_mhead)
  2797 	with eq_mhds
  2798 	show ?thesis  
  2799 	  by (cases emh) auto
  2800       qed
  2801       with statT dynC_prop
  2802       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2803 	by simp
  2804       with isT_statT statT
  2805       have isif_I: "is_iface G I"
  2806 	by simp
  2807       from dynM statT
  2808       have dynM': "dynimethd G I dynC sig = Some dynM"
  2809 	by (simp add: dynlookup_def) 
  2810       from False implmnt isif_I wf dynM'
  2811       show ?thesis
  2812 	by - (drule implmt_dynimethd_access, auto)
  2813     qed
  2814   next
  2815     case (Array_Object_methd T statM)
  2816     assume statT: "statT = ArrayT T"
  2817     assume "accmethd G accC Object sig = Some statM"
  2818     then have    statM: "methd G Object sig = Some statM" and
  2819               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2820       by (auto dest: accmethd_SomeD)
  2821     from statT dynC_prop
  2822     have dynC_Obj: "dynC = Object" 
  2823       by simp
  2824     then
  2825     have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object"
  2826       by simp
  2827     from dynM statT    
  2828     have dynM': "dynmethd G Object dynC sig = Some dynM"
  2829       by (simp add: dynlookup_def)
  2830     from statM statT_acc stat_acc dynM' wf widen_dynC_Obj  
  2831          statT isT_statT  
  2832     show ?thesis   
  2833       by - (drule dynmethd_access_prop, simp+) 
  2834   qed
  2835 qed
  2836 
  2837 lemma dynlookup_access:
  2838  (assumes emh: "emh \<in> mheads G accC statT sig" and
  2839     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
  2840     isT_statT: "isrtype G statT" and
  2841            wf: "wf_prog G"
  2842  ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
  2843             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2844 proof - 
  2845   from dynC_prop isT_statT wf
  2846   have is_cls_dynC: "is_class G dynC"
  2847     by (auto dest: valid_lookup_cls_is_class)
  2848   with emh wf dynC_prop isT_statT
  2849   obtain dynM where 
  2850     "dynlookup G statT dynC sig = Some dynM"
  2851     by - (drule dynamic_mheadsD,auto)
  2852   with  emh dynC_prop isT_statT wf
  2853   show ?thesis 
  2854     by (blast intro: dynlookup_access_prop)
  2855 qed
  2856 
  2857 lemma stat_overrides_Package_old: 
  2858 (assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
  2859           accmodi_new: "accmodi new = Package" and
  2860                    wf: "wf_prog G "
  2861 ) "accmodi old = Package"
  2862 proof -
  2863   from stat_override wf 
  2864   have "accmodi old \<le> accmodi new"
  2865     by (auto dest: wf_prog_stat_overridesD)
  2866   with stat_override accmodi_new show ?thesis
  2867     by (cases "accmodi old") (auto dest: no_Private_stat_override 
  2868                                    dest: acc_modi_le_Dests)
  2869 qed
  2870 
  2871 text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
  2872 Without it. it is easy to leaf the Package!
  2873 *}
  2874 lemma dyn_accessible_Package:
  2875  "\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package;
  2876    wf_prog G\<rbrakk>
  2877   \<Longrightarrow> pid accC = pid (declclass m)"
  2878 proof -
  2879   assume wf: "wf_prog G "
  2880   assume accessible: "G \<turnstile> m in C dyn_accessible_from accC"
  2881   then show "accmodi m = Package 
  2882             \<Longrightarrow> pid accC = pid (declclass m)"
  2883     (is "?Pack m \<Longrightarrow> ?P m")
  2884   proof (induct rule: dyn_accessible_fromR.induct)
  2885     case (Immediate C m)
  2886     assume "G\<turnstile>m member_in C"
  2887            "G \<turnstile> m in C permits_acc_to accC"
  2888            "accmodi m = Package"      
  2889     then show "?P m"
  2890       by (auto simp add: permits_acc_def)
  2891   next
  2892     case (Overriding declC C new newm old Sup)
  2893     assume member_new: "G \<turnstile> new member_in C" and
  2894                   new: "new = (declC, mdecl newm)" and
  2895              override: "G \<turnstile> (declC, newm) overrides old" and
  2896          subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
  2897               acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and
  2898                   hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and
  2899           accmodi_new: "accmodi new = Package"
  2900     from override accmodi_new new wf 
  2901     have accmodi_old: "accmodi old = Package"  
  2902       by (auto dest: overrides_Package_old)
  2903     with hyp 
  2904     have P_sup: "?P (methdMembr old)"
  2905       by (simp)
  2906     from wf override new accmodi_old accmodi_new
  2907     have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
  2908       by (auto dest: dyn_override_Package)
  2909     with eq_pid_new_old P_sup show "?P new"
  2910       by auto
  2911   qed
  2912 qed
  2913 
  2914 
  2915 text {* @{text dyn_accessible_instance_field_Protected} only works for fields
  2916 since methods can break the package bounds due to overriding
  2917 *}
  2918 lemma dyn_accessible_instance_field_Protected:
  2919  (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
  2920              prot: "accmodi f = Protected" and
  2921             field: "is_field f" and
  2922    instance_field: "\<not> is_static f" and
  2923           outside: "pid (declclass f) \<noteq> pid accC"
  2924  ) "G\<turnstile> C \<preceq>\<^sub>C accC"
  2925 proof -
  2926   from dyn_acc prot field instance_field outside
  2927   show ?thesis
  2928   proof (induct)
  2929     case (Immediate C f)
  2930     have "G \<turnstile> f in C permits_acc_to accC" .
  2931     moreover 
  2932     assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
  2933            "pid (declclass f) \<noteq> pid accC"
  2934     ultimately 
  2935     show "G\<turnstile> C \<preceq>\<^sub>C accC"
  2936       by (auto simp add: permits_acc_def)
  2937   next
  2938     case Overriding
  2939     then show ?case by (simp add: is_field_def)
  2940   qed
  2941 qed
  2942    
  2943 lemma dyn_accessible_static_field_Protected:
  2944  (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
  2945              prot: "accmodi f = Protected" and
  2946             field: "is_field f" and
  2947      static_field: "is_static f" and
  2948           outside: "pid (declclass f) \<noteq> pid accC"
  2949  ) "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
  2950 proof -
  2951   from dyn_acc prot field static_field outside
  2952   show ?thesis
  2953   proof (induct)
  2954     case (Immediate C f)
  2955     assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
  2956            "pid (declclass f) \<noteq> pid accC"
  2957     moreover 
  2958     have "G \<turnstile> f in C permits_acc_to accC" .
  2959     ultimately
  2960     have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
  2961       by (auto simp add: permits_acc_def)
  2962     moreover
  2963     have "G \<turnstile> f member_in C" .
  2964     then have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
  2965       by (rule member_in_class_relation)
  2966     ultimately show ?case
  2967       by blast
  2968   next
  2969     case Overriding
  2970     then show ?case by (simp add: is_field_def)
  2971   qed
  2972 qed
  2973 
  2974 end