src/HOL/Bali/WellForm.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/WellForm.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     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   (* 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> nodups (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 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); nodups (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 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 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 declare split_paired_All [simp del] split_paired_Ex [simp del]
  1295 ML_setup {*
  1296 simpset_ref() := simpset() delloop "split_all_tac";
  1297 claset_ref () := claset () delSWrapper "split_all_tac"
  1298 *}
  1299 
  1300 lemma declclass_widen[rule_format]: 
  1301  "wf_prog G 
  1302  \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1303  \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1304 proof (rule class_rec.induct,intro allI impI)
  1305   fix G C c m
  1306   assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
  1307                \<longrightarrow> ?P G (super c)"
  1308   assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  1309          m:  "methd G C sig = Some m"
  1310   show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
  1311   proof (cases "C=Object")
  1312     case True 
  1313     with wf m show ?thesis by (simp add: methd_Object_SomeD)
  1314   next
  1315     let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  1316     let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1317     case False 
  1318     with cls_C wf m
  1319     have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  1320       by (simp add: methd_rec)
  1321     show ?thesis
  1322     proof (cases "?table sig")
  1323       case None
  1324       from this methd_C have "?filter (methd G (super c)) sig = Some m"
  1325 	by simp
  1326       moreover
  1327       from wf cls_C False obtain sup where "class G (super c) = Some sup"
  1328 	by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1329       moreover note wf False cls_C Hyp 
  1330       ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  by auto
  1331       moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I)
  1332       ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
  1333     next
  1334       case Some
  1335       from this wf False cls_C methd_C show ?thesis by auto
  1336     qed
  1337   qed
  1338 qed
  1339 
  1340 (*
  1341 lemma declclass_widen[rule_format]: 
  1342  "wf_prog G 
  1343  \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1344  \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1345 apply (rule class_rec.induct)
  1346 apply (rule impI)+
  1347 apply (case_tac "C=Object")
  1348 apply   (force simp add: methd_Object_SomeD)
  1349 
  1350 apply   (rule allI)+
  1351 apply   (rule impI)
  1352 apply   (simp (no_asm_simp) add: methd_rec)
  1353 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
  1354 apply    (simp add: override_def)
  1355 apply    (frule (1) subcls1I)
  1356 apply    (drule (1) wf_prog_cdecl)
  1357 apply    (drule (1) wf_cdecl_supD)
  1358 apply    clarify
  1359 apply    (drule is_acc_class_is_class)
  1360 apply    clarify
  1361 apply    (blast dest: rtrancl_into_rtrancl2)
  1362 
  1363 apply    auto
  1364 done
  1365 *)
  1366 
  1367 (*
  1368 lemma accessible_public_inheritance_lemma1:
  1369   "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object; accmodi m = Public;
  1370     G\<turnstile>m accessible_through_inheritance_in (super c)\<rbrakk> 
  1371    \<Longrightarrow> G\<turnstile>m accessible_through_inheritance_in C"
  1372 apply   (frule (1) subcls1I)
  1373 apply   (rule accessible_through_inheritance.Indirect)
  1374 apply     (blast)
  1375 apply     (erule accessible_through_inheritance_subclsD)
  1376 apply     (blast dest: wf_prog_acc_superD is_acc_classD)
  1377 apply     assumption
  1378 apply     (force dest: wf_prog_acc_superD is_acc_classD
  1379                  simp add: accessible_for_inheritance_in_def)
  1380 done
  1381 
  1382 lemma accessible_public_inheritance_lemma[rule_format]:
  1383   "\<lbrakk>wf_prog G;C \<noteq> Object; class G C = Some c; 
  1384     accmodi m = Public
  1385    \<rbrakk> \<Longrightarrow> methd G (super c) sig = Some m 
  1386         \<longrightarrow> G\<turnstile>m accessible_through_inheritance_in C" 
  1387 apply (frule (2) wf_prog_acc_superD [THEN is_acc_classD])
  1388 apply (erule conjE)
  1389 apply (simp only: not_None_eq)
  1390 apply (erule exE)
  1391 apply (case_tac "(super c) = Object")
  1392 apply   (rule impI)
  1393 apply   (rule accessible_through_inheritance.Direct)
  1394 apply     force
  1395 apply     (force simp add: accessible_for_inheritance_in_def)
  1396 
  1397 apply   (frule wf_ws_prog) 
  1398 apply   (simp add: methd_rec)
  1399 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, super c, m)) (methods y)) sig")
  1400 apply     simp
  1401 apply     (clarify)
  1402 apply     (rule_tac D="super c" in accessible_through_inheritance.Indirect)
  1403 apply       (blast dest: subcls1I)
  1404 apply       (blast)
  1405 apply       simp
  1406 apply       assumption
  1407 apply       (simp add: accessible_for_inheritance_in_def)
  1408 
  1409 apply     clarsimp
  1410 apply     (rule accessible_through_inheritance.Direct)
  1411 apply     (auto dest: subcls1I simp add: accessible_for_inheritance_in_def)
  1412 done
  1413 
  1414 lemma accessible_public_inheritance:
  1415   "\<lbrakk>wf_prog G; class G D = Some d; G\<turnstile>C \<prec>\<^sub>C D; methd G D sig = Some m; 
  1416     accmodi m = Public\<rbrakk> 
  1417    \<Longrightarrow> G \<turnstile> m accessible_through_inheritance_in C"
  1418 apply (erule converse_trancl_induct)
  1419 apply  (blast dest: subcls1D intro: accessible_public_inheritance_lemma)
  1420 
  1421 apply  (frule subcls1D)
  1422 apply  clarify
  1423 apply  (frule  (2) wf_prog_acc_superD [THEN is_acc_classD])
  1424 apply  clarify
  1425 apply  (rule_tac D="super c" in accessible_through_inheritance.Indirect)
  1426 apply   (auto intro:trancl_into_trancl2 
  1427                     accessible_through_inheritance_subclsD
  1428               simp add: accessible_for_inheritance_in_def)
  1429 done
  1430 *)
  1431 
  1432 
  1433 lemma declclass_methd_Object: 
  1434  "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object"
  1435 by auto
  1436 
  1437 
  1438 lemma methd_declaredD: 
  1439  "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 
  1440   \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1441 proof -
  1442   assume    wf: "wf_prog G"
  1443   then have ws: "ws_prog G" ..
  1444   assume  clsC: "is_class G C"
  1445   from clsC ws 
  1446   show "methd G C sig = Some m 
  1447         \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1448     (is "PROP ?P C") 
  1449   proof (induct ?P C rule: ws_class_induct')
  1450     case Object
  1451     assume "methd G Object sig = Some m" 
  1452     with wf show ?thesis
  1453       by - (rule method_declared_inI, auto) 
  1454   next
  1455     case Subcls
  1456     fix C c
  1457     assume clsC: "class G C = Some c"
  1458     and       m: "methd G C sig = Some m"
  1459     and     hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 
  1460     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1461     show ?thesis
  1462     proof (cases "?newMethods sig")
  1463       case None
  1464       from None ws clsC m hyp 
  1465       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
  1466     next
  1467       case Some
  1468       from Some ws clsC m 
  1469       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
  1470     qed
  1471   qed
  1472 qed
  1473 
  1474 
  1475 lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
  1476 (assumes methd_C: "methd G C sig = Some m" and
  1477                     ws: "ws_prog G" and
  1478                   clsC: "class G C = Some c" and
  1479              neq_C_Obj: "C\<noteq>Object" )  
  1480 "\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
  1481   \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
  1482  \<rbrakk> \<Longrightarrow> P"
  1483 proof -
  1484   let ?inherited   = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 
  1485                               (methd G (super c))"
  1486   let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1487   from ws clsC neq_C_Obj methd_C 
  1488   have methd_unfold: "(?inherited ++ ?new) sig = Some m"
  1489     by (simp add: methd_rec)
  1490   assume NewMethod: "?new sig = Some m \<Longrightarrow> P"
  1491   assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); 
  1492                             methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P"
  1493   show P
  1494   proof (cases "?new sig")
  1495     case None
  1496     with methd_unfold have "?inherited sig = Some m"
  1497       by (auto)
  1498     with InheritedMethod show P by blast
  1499   next
  1500     case Some
  1501     with methd_unfold have "?new sig = Some m"
  1502       by auto
  1503     with NewMethod show P by blast
  1504   qed
  1505 qed
  1506 
  1507   
  1508 lemma methd_member_of:
  1509  (assumes wf: "wf_prog G") 
  1510   "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
  1511   (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
  1512 proof -
  1513   from wf   have   ws: "ws_prog G" ..
  1514   assume defC: "is_class G C"
  1515   from defC ws 
  1516   show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
  1517   proof (induct rule: ws_class_induct')  
  1518     case Object
  1519     with wf have declC: "declclass m = Object"
  1520       by (blast intro: declclass_methd_Object)
  1521     with Object wf have "G\<turnstile>Methd sig m declared_in Object"
  1522       by (auto dest: methd_declaredD simp del: methd_Object)
  1523     with declC 
  1524     show "?MemberOf Object"
  1525       by (auto intro!: members.Immediate
  1526                   simp del: methd_Object)
  1527   next
  1528     case (Subcls C c)
  1529     assume  clsC: "class G C = Some c" and
  1530        neq_C_Obj: "C \<noteq> Object"  
  1531     assume methd: "?Method C"
  1532     from methd ws clsC neq_C_Obj
  1533     show "?MemberOf C"
  1534     proof (cases rule: methd_rec_Some_cases)
  1535       case NewMethod
  1536       with clsC show ?thesis
  1537 	by (auto dest: method_declared_inI intro!: members.Immediate)
  1538     next
  1539       case InheritedMethod
  1540       then show "?thesis"
  1541 	by (blast dest: inherits_member)
  1542     qed
  1543   qed
  1544 qed
  1545 
  1546 lemma current_methd: 
  1547       "\<lbrakk>table_of (methods c) sig = Some new;
  1548         ws_prog G; class G C = Some c; C \<noteq> Object; 
  1549         methd G (super c) sig = Some old\<rbrakk> 
  1550     \<Longrightarrow> methd G C sig = Some (C,new)"
  1551 by (auto simp add: methd_rec
  1552             intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
  1553 
  1554 lemma wf_prog_staticD:
  1555  (assumes     wf: "wf_prog G" and 
  1556             clsC: "class G C = Some c" and
  1557        neq_C_Obj: "C \<noteq> Object" and 
  1558              old: "methd G (super c) sig = Some old" and 
  1559      accmodi_old: "Protected \<le> accmodi old" and
  1560              new: "table_of (methods c) sig = Some new"
  1561  ) "is_static new = is_static old"
  1562 proof -
  1563   from clsC wf 
  1564   have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
  1565   from wf clsC neq_C_Obj
  1566   have is_cls_super: "is_class G (super c)" 
  1567     by (blast dest: wf_prog_acc_superD is_acc_classD)
  1568   from wf is_cls_super old 
  1569   have old_member_of: "G\<turnstile>Methd sig old member_of (super c)"  
  1570     by (rule methd_member_of)
  1571   from old wf is_cls_super 
  1572   have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)"
  1573     by (auto dest: methd_declared_in_declclass)
  1574   from new clsC 
  1575   have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C"
  1576     by (auto intro: method_declared_inI)
  1577   note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
  1578   from clsC neq_C_Obj
  1579   have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1580     by (rule subcls1I)
  1581   then have "G\<turnstile>C \<prec>\<^sub>C super c" ..
  1582   also from old wf is_cls_super
  1583   have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC)
  1584   finally have subcls_C_old:  "G\<turnstile>C \<prec>\<^sub>C (declclass old)" .
  1585   from accmodi_old 
  1586   have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C"
  1587     by (auto simp add: inheritable_in_def
  1588                  dest: acc_modi_le_Dests)
  1589   show ?thesis
  1590   proof (cases "is_static new")
  1591     case True
  1592     with subcls_C_old new_declared old_declared inheritable
  1593     have "G,sig\<turnstile>(C,new) hides old"
  1594       by (auto intro: hidesI)
  1595     with True wf_cdecl neq_C_Obj new 
  1596     show ?thesis
  1597       by (auto dest: wf_cdecl_hides_SomeD)
  1598   next
  1599     case False
  1600     with subcls_C_old new_declared old_declared inheritable subcls1_C_super
  1601          old_member_of
  1602     have "G,sig\<turnstile>(C,new) overrides\<^sub>S old"
  1603       by (auto intro: stat_overridesR.Direct)
  1604     with False wf_cdecl neq_C_Obj new 
  1605     show ?thesis
  1606       by (auto dest: wf_cdecl_overrides_SomeD)
  1607   qed
  1608 qed
  1609 
  1610 lemma inheritable_instance_methd: 
  1611  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1612               is_cls_D: "is_class G D" and
  1613                     wf: "wf_prog G" and 
  1614                    old: "methd G D sig = Some old" and
  1615            accmodi_old: "Protected \<le> accmodi old" and  
  1616         not_static_old: "\<not> is_static old"
  1617  )  
  1618   "\<exists>new. methd G C sig = Some new \<and>
  1619          (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
  1620  (is "(\<exists>new. (?Constraint C new old))")
  1621 proof -
  1622   from subclseq_C_D is_cls_D 
  1623   have is_cls_C: "is_class G C" by (rule subcls_is_class2) 
  1624   from wf 
  1625   have ws: "ws_prog G" ..
  1626   from is_cls_C ws subclseq_C_D 
  1627   show "\<exists>new. ?Constraint C new old"
  1628   proof (induct rule: ws_class_induct')
  1629     case (Object co)
  1630     then have eq_D_Obj: "D=Object" by auto
  1631     with old 
  1632     have "?Constraint Object old old"
  1633       by auto
  1634     with eq_D_Obj 
  1635     show "\<exists> new. ?Constraint Object new old" by auto
  1636   next
  1637     case (Subcls C c)
  1638     assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old"
  1639     assume clsC: "class G C = Some c"
  1640     assume neq_C_Obj: "C\<noteq>Object"
  1641     from clsC wf 
  1642     have wf_cdecl: "wf_cdecl G (C,c)" 
  1643       by (rule wf_prog_cdecl)
  1644     from ws clsC neq_C_Obj
  1645     have is_cls_super: "is_class G (super c)"
  1646       by (auto dest: ws_prog_cdeclD)
  1647     from clsC wf neq_C_Obj 
  1648     have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and
  1649 	 subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
  1650       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
  1651               intro: subcls1I)
  1652     show "\<exists>new. ?Constraint C new old"
  1653     proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D")
  1654       case False
  1655       from False Subcls 
  1656       have eq_C_D: "C=D"
  1657 	by (auto dest: subclseq_superD)
  1658       with old 
  1659       have "?Constraint C old old"
  1660 	by auto
  1661       with eq_C_D 
  1662       show "\<exists> new. ?Constraint C new old" by auto
  1663     next
  1664       case True
  1665       with hyp obtain super_method
  1666 	where super: "?Constraint (super c) super_method old" by blast
  1667       from super not_static_old
  1668       have not_static_super: "\<not> is_static super_method"
  1669 	by (auto dest!: stat_overrides_commonD)
  1670       from super old wf accmodi_old
  1671       have accmodi_super_method: "Protected \<le> accmodi super_method"
  1672 	by (auto dest!: wf_prog_stat_overridesD
  1673                  intro: order_trans)
  1674       from super accmodi_old wf
  1675       have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
  1676 	by (auto dest!: wf_prog_stat_overridesD
  1677                         acc_modi_le_Dests
  1678               simp add: inheritable_in_def)	           
  1679       from super wf is_cls_super
  1680       have member: "G\<turnstile>Methd sig super_method member_of (super c)"
  1681 	by (auto intro: methd_member_of) 
  1682       from member
  1683       have decl_super_method:
  1684         "G\<turnstile>Methd sig super_method declared_in (declclass super_method)"
  1685 	by (auto dest: member_of_declC)
  1686       from super subcls1_C_super ws is_cls_super 
  1687       have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)"
  1688 	by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 
  1689       show "\<exists> new. ?Constraint C new old"
  1690       proof (cases "methd G C sig")
  1691 	case None
  1692 	have "methd G (super c) sig = None"
  1693 	proof -
  1694 	  from clsC ws None 
  1695 	  have no_new: "table_of (methods c) sig = None" 
  1696 	    by (auto simp add: methd_rec)
  1697 	  with clsC 
  1698 	  have undeclared: "G\<turnstile>mid sig undeclared_in C"
  1699 	    by (auto simp add: undeclared_in_def cdeclaredmethd_def)
  1700 	  with inheritable member superAccessible subcls1_C_super
  1701 	  have inherits: "G\<turnstile>C inherits (method sig super_method)"
  1702 	    by (auto simp add: inherits_def)
  1703 	  with clsC ws no_new super neq_C_Obj
  1704 	  have "methd G C sig = Some super_method"
  1705 	    by (auto simp add: methd_rec override_def
  1706 	                intro: filter_tab_SomeI)
  1707           with None show ?thesis
  1708 	    by simp
  1709 	qed
  1710 	with super show ?thesis by auto
  1711       next
  1712 	case (Some new)
  1713 	from this ws clsC neq_C_Obj
  1714 	show ?thesis
  1715 	proof (cases rule: methd_rec_Some_cases)
  1716 	  case InheritedMethod
  1717 	  with super Some show ?thesis 
  1718 	    by auto
  1719 	next
  1720 	  case NewMethod
  1721 	  assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig 
  1722                        = Some new"
  1723 	  from new 
  1724 	  have declcls_new: "declclass new = C" 
  1725 	    by auto
  1726 	  from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
  1727 	  have not_static_new: "\<not> is_static new" 
  1728 	    by (auto dest: wf_prog_staticD) 
  1729 	  from clsC new
  1730 	  have decl_new: "G\<turnstile>Methd sig new declared_in C"
  1731 	    by (auto simp add: declared_in_def cdeclaredmethd_def)
  1732 	  from not_static_new decl_new decl_super_method
  1733 	       member subcls1_C_super inheritable declcls_new subcls_C_super 
  1734 	  have "G,sig\<turnstile> new overrides\<^sub>S super_method"
  1735 	    by (auto intro: stat_overridesR.Direct) 
  1736 	  with super Some
  1737 	  show ?thesis
  1738 	    by (auto intro: stat_overridesR.Indirect)
  1739 	qed
  1740       qed
  1741     qed
  1742   qed
  1743 qed
  1744 
  1745 lemma inheritable_instance_methd_cases [consumes 6
  1746                                        , case_names Inheritance Overriding]: 
  1747  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1748               is_cls_D: "is_class G D" and
  1749                     wf: "wf_prog G" and 
  1750                    old: "methd G D sig = Some old" and
  1751            accmodi_old: "Protected \<le> accmodi old" and  
  1752         not_static_old: "\<not> is_static old" and
  1753            inheritance:  "methd G C sig = Some old \<Longrightarrow> P" and
  1754             overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
  1755                                    G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
  1756         
  1757  ) "P"
  1758 proof -
  1759 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1760      inheritance overriding
  1761 show ?thesis
  1762   by (auto dest: inheritable_instance_methd)
  1763 qed
  1764 
  1765 lemma inheritable_instance_methd_props: 
  1766  (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1767               is_cls_D: "is_class G D" and
  1768                     wf: "wf_prog G" and 
  1769                    old: "methd G D sig = Some old" and
  1770            accmodi_old: "Protected \<le> accmodi old" and  
  1771         not_static_old: "\<not> is_static old"
  1772  )  
  1773   "\<exists>new. methd G C sig = Some new \<and>
  1774           \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
  1775  (is "(\<exists>new. (?Constraint C new old))")
  1776 proof -
  1777   from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1778   show ?thesis
  1779   proof (cases rule: inheritable_instance_methd_cases)
  1780     case Inheritance
  1781     with not_static_old accmodi_old show ?thesis by auto
  1782   next
  1783     case (Overriding new)
  1784     then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
  1785     with Overriding not_static_old accmodi_old wf 
  1786     show ?thesis 
  1787       by (auto dest!: wf_prog_stat_overridesD
  1788                intro: order_trans)
  1789   qed
  1790 qed
  1791  	  
  1792 (* ### Probleme: Die tollen methd_subcls_cases Lemma wird warscheinlich
  1793   kaum gebraucht: 
  1794 Redundanz: stat_overrides.Direct old declared in declclass old folgt aus
  1795            member of 
  1796    Problem: Predikate wie overrides, sind global üper die Hierarchie hinweg
  1797             definiert, aber oft barucht man eben zusätlich Induktion
  1798             : von super c auf C; Dann ist aber auss dem Kontext
  1799             die Unterscheidung in die 5 fälle overkill,
  1800             da man dann warscheinlich meistens eh in einem speziellen
  1801             Fall kommt (durch die Hypothesen)
  1802 *)
  1803     
  1804 (* local lemma *)
  1805 ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
  1806 ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
  1807 lemma subint_widen_imethds: 
  1808  "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow>   
  1809   \<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> 
  1810                           accmodi im = accmodi jm \<and>
  1811                           G\<turnstile>resTy im\<preceq>resTy jm"
  1812 proof -
  1813   assume irel: "G\<turnstile>I\<preceq>I J" and
  1814            wf: "wf_prog G" and
  1815      is_iface: "is_iface G J"
  1816   from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" 
  1817                (is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I")
  1818   proof (induct ?P I rule: converse_rtrancl_induct) 
  1819     case Id
  1820     assume "jm \<in> imethds G J sig"
  1821     then show "?Concl J" by  (blast elim: bexI')
  1822   next
  1823     case Step
  1824     fix I SI
  1825     assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and 
  1826             subint_SI_J: "G\<turnstile>SI \<preceq>I J" and
  1827                     hyp: "PROP ?P SI" and
  1828                      jm: "jm \<in> imethds G J sig"
  1829     from subint1_I_SI 
  1830     obtain i where
  1831       ifI: "iface G I = Some i" and
  1832        SI: "SI \<in> set (isuperIfs i)"
  1833       by (blast dest: subint1D)
  1834 
  1835     let ?newMethods 
  1836           = "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
  1837     show "?Concl I"
  1838     proof (cases "?newMethods sig = {}")
  1839       case True
  1840       with ifI SI hyp wf jm 
  1841       show "?thesis" 
  1842 	by (auto simp add: imethds_rec) 
  1843     next
  1844       case False
  1845       from ifI wf False
  1846       have imethds: "imethds G I sig = ?newMethods sig"
  1847 	by (simp add: imethds_rec)
  1848       from False
  1849       obtain im where
  1850         imdef: "im \<in> ?newMethods sig" 
  1851 	by (blast)
  1852       with imethds 
  1853       have im: "im \<in> imethds G I sig"
  1854 	by (blast)
  1855       with im wf ifI 
  1856       obtain
  1857 	 imStatic: "\<not> is_static im" and
  1858          imPublic: "accmodi im = Public"
  1859 	by (auto dest!: imethds_wf_mhead)	
  1860       from ifI wf 
  1861       have wf_I: "wf_idecl G (I,i)" 
  1862 	by (rule wf_prog_idecl)
  1863       with SI wf  
  1864       obtain si where
  1865 	 ifSI: "iface G SI = Some si" and
  1866 	wf_SI: "wf_idecl G (SI,si)" 
  1867 	by (auto dest!: wf_idecl_supD is_acc_ifaceD
  1868                   dest: wf_prog_idecl)
  1869       from jm hyp 
  1870       obtain sim::"qtname \<times> mhead"  where
  1871                       sim: "sim \<in> imethds G SI sig" and
  1872          eq_static_sim_jm: "is_static sim = is_static jm" and 
  1873          eq_access_sim_jm: "accmodi sim = accmodi jm" and 
  1874         resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm"
  1875 	by blast
  1876       with wf_I SI imdef sim 
  1877       have "G\<turnstile>resTy im\<preceq>resTy sim"   
  1878 	by (auto dest!: wf_idecl_hidings hidings_entailsD)
  1879       with wf resTy_widen_sim_jm 
  1880       have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm"
  1881 	by (blast intro: widen_trans)
  1882       from sim wf ifSI  
  1883       obtain
  1884 	simStatic: "\<not> is_static sim" and
  1885         simPublic: "accmodi sim = Public"
  1886 	by (auto dest!: imethds_wf_mhead)
  1887       from im 
  1888            imStatic simStatic eq_static_sim_jm
  1889            imPublic simPublic eq_access_sim_jm
  1890            resTy_widen_im_jm
  1891       show ?thesis 
  1892 	by auto 
  1893     qed
  1894   qed
  1895 qed
  1896      
  1897 (* Tactical version *)
  1898 (* 
  1899 lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow>  
  1900   \<forall> jm \<in> imethds G J sig.  
  1901   \<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> 
  1902                           access (mthd im)= access (mthd jm) \<and>
  1903                           G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)"
  1904 apply (erule converse_rtrancl_induct)
  1905 apply  (clarsimp elim!: bexI')
  1906 apply (frule subint1D)
  1907 apply clarify
  1908 apply (erule ballE')
  1909 apply  fast
  1910 apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl)
  1911 apply clarsimp
  1912 apply (subst imethds_rec, assumption, erule wf_ws_prog)
  1913 apply (unfold overrides_t_def)
  1914 apply (drule (1) wf_prog_idecl)
  1915 apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
  1916                                        [THEN is_acc_ifaceD [THEN conjunct1]]]])
  1917 apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
  1918                   sig ={}")
  1919 apply   force
  1920 
  1921 apply   (simp only:)
  1922 apply   (simp)
  1923 apply   clarify
  1924 apply   (frule wf_idecl_hidings [THEN hidings_entailsD])
  1925 apply     blast
  1926 apply     blast
  1927 apply   (rule bexI')
  1928 apply     simp
  1929 apply     (drule table_of_map_SomeI [of _ "sig"])
  1930 apply     simp
  1931 
  1932 apply     (frule wf_idecl_mhead [of _ _ _ "sig"])
  1933 apply       (rule table_of_Some_in_set)
  1934 apply       assumption
  1935 apply     auto
  1936 done
  1937 *)
  1938     
  1939 
  1940 (* local lemma *)
  1941 lemma implmt1_methd: 
  1942  "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow>  
  1943   \<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> 
  1944                        G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1945                        accmodi im = Public \<and> accmodi cm = Public"
  1946 apply (drule implmt1D)
  1947 apply clarify
  1948 apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
  1949 apply (frule (1) imethds_wf_mhead)
  1950 apply  (simp add: is_acc_iface_def)
  1951 apply (force)
  1952 done
  1953 
  1954 
  1955 (* local lemma *)
  1956 lemma implmt_methd [rule_format (no_asm)]: 
  1957 "\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow>  
  1958  (\<forall> im    \<in>imethds G I   sig.  
  1959   \<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> 
  1960                       G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1961                       accmodi im = Public \<and> accmodi cm = Public)"
  1962 apply (frule implmt_is_class)
  1963 apply (erule implmt.induct)
  1964 apply   safe
  1965 apply   (drule (2) implmt1_methd)
  1966 apply   fast
  1967 apply  (drule (1) subint_widen_imethds)
  1968 apply   simp
  1969 apply   assumption
  1970 apply  clarify
  1971 apply  (drule (2) implmt1_methd)
  1972 apply  (force)
  1973 apply (frule subcls1D)
  1974 apply (drule (1) bspec)
  1975 apply clarify
  1976 apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 
  1977                                  OF _ implmt_is_class])
  1978 apply auto 
  1979 done
  1980 
  1981 
  1982 declare split_paired_All [simp] split_paired_Ex [simp]
  1983 ML_setup {*
  1984 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  1985 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  1986 *}
  1987 lemma mheadsD [rule_format (no_asm)]: 
  1988 "emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow>
  1989  (\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> 
  1990           accmethd G S C sig = Some m \<and>
  1991           (declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or>
  1992  (\<exists>I. t = IfaceT I \<and> ((\<exists>im. im  \<in> accimethds G (pid S) I sig \<and> 
  1993           mthd im = mhd emh) \<or> 
  1994   (\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> 
  1995        accmodi m \<noteq> Private \<and> 
  1996        declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or>
  1997  (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
  1998         accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 
  1999         declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
  2000 apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1])
  2001 apply auto
  2002 apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
  2003 apply (auto  dest!: accmethd_SomeD)
  2004 done
  2005 
  2006 lemma mheads_cases [consumes 2, case_names Class_methd 
  2007                     Iface_methd Iface_Object_methd Array_Object_methd]: 
  2008 "\<lbrakk>emh \<in> mheads G S t sig; wf_prog G;
  2009  \<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m;
  2010            (declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh; 
  2011  \<And> I im. \<lbrakk>t = IfaceT I; im  \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk>
  2012           \<Longrightarrow> P emh;
  2013  \<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S);
  2014           accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
  2015          declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh;
  2016  \<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S);
  2017           accmethd G S Object sig = Some m; accmodi m \<noteq> Private; 
  2018           declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow>  P emh 
  2019 \<rbrakk> \<Longrightarrow> P emh"
  2020 by (blast dest!: mheadsD)
  2021 
  2022 lemma declclassD[rule_format]:
  2023  "\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; 
  2024    class G (declclass m) = Some d\<rbrakk>
  2025   \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)"
  2026 proof -
  2027   assume    wf: "wf_prog G"
  2028   then have ws: "ws_prog G" ..
  2029   assume  clsC: "class G C = Some c"
  2030   from clsC ws 
  2031   show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
  2032         \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
  2033          (is "PROP ?P C") 
  2034   proof (induct ?P C rule: ws_class_induct)
  2035     case Object
  2036     fix m d
  2037     assume "methd G Object sig = Some m" 
  2038            "class G (declclass m) = Some d"
  2039     with wf show "?thesis m d" by auto
  2040   next
  2041     case Subcls
  2042     fix C c m d
  2043     assume hyp: "PROP ?P (super c)"
  2044     and      m: "methd G C sig = Some m"
  2045     and  declC: "class G (declclass m) = Some d"
  2046     and   clsC: "class G C = Some c"
  2047     and   nObj: "C \<noteq> Object"
  2048     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
  2049     show "?thesis m d" 
  2050     proof (cases "?newMethods")
  2051       case None
  2052       from None clsC nObj ws m declC hyp  
  2053       show "?thesis" by (auto simp add: methd_rec)
  2054     next
  2055       case Some
  2056       from Some clsC nObj ws m declC hyp  
  2057       show "?thesis" 
  2058 	by (auto simp add: methd_rec
  2059                      dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  2060     qed
  2061   qed
  2062 qed
  2063 
  2064 (* Tactical version *)
  2065 (*
  2066 lemma declclassD[rule_format]:
  2067  "wf_prog G \<longrightarrow>  
  2068  (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
  2069   class G (declclass m) = Some d
  2070  \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
  2071 apply (rule class_rec.induct)
  2072 apply (rule impI)
  2073 apply (rule allI)+
  2074 apply (rule impI)
  2075 apply (case_tac "C=Object")
  2076 apply   (force simp add: methd_rec)
  2077 
  2078 apply   (subst methd_rec)
  2079 apply     (blast dest: wf_ws_prog)+
  2080 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
  2081 apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  2082 done
  2083 *)
  2084 
  2085 lemma dynmethd_Object:
  2086  (assumes statM: "methd G Object sig = Some statM" and
  2087         private: "accmodi statM = Private" and 
  2088        is_cls_C: "is_class G C" and
  2089              wf: "wf_prog G"
  2090  ) "dynmethd G Object C sig = Some statM"
  2091 proof -
  2092   from is_cls_C wf 
  2093   have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
  2094     by (auto intro: subcls_ObjectI)
  2095   from wf have ws: "ws_prog G" 
  2096     by simp
  2097   from wf 
  2098   have is_cls_Obj: "is_class G Object" 
  2099     by simp
  2100   from statM subclseq is_cls_Obj ws private
  2101   show ?thesis
  2102   proof (cases rule: dynmethd_cases)
  2103     case Static then show ?thesis .
  2104   next
  2105     case Overrides 
  2106     with private show ?thesis 
  2107       by (auto dest: no_Private_override)
  2108   qed
  2109 qed
  2110 
  2111 lemma wf_imethds_hiding_objmethdsD: 
  2112   (assumes     old: "methd G Object sig = Some old" and
  2113            is_if_I: "is_iface G I" and
  2114                 wf: "wf_prog G" and    
  2115        not_private: "accmodi old \<noteq> Private" and
  2116                new: "new \<in> imethds G I sig" 
  2117   ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
  2118 proof -
  2119   from wf have ws: "ws_prog G" by simp
  2120   {
  2121     fix I i new
  2122     assume ifI: "iface G I = Some i"
  2123     assume new: "table_of (imethods i) sig = Some new" 
  2124     from ifI new not_private wf old  
  2125     have "?P (I,new)"
  2126       by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
  2127             simp del: methd_Object)
  2128   } note hyp_newmethod = this  
  2129   from is_if_I ws new 
  2130   show ?thesis
  2131   proof (induct rule: ws_interface_induct)
  2132     case (Step I i)
  2133     assume ifI: "iface G I = Some i" 
  2134     assume new: "new \<in> imethds G I sig" 
  2135     from Step
  2136     have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)"
  2137       by auto 
  2138     from new ifI ws
  2139     show "?P new"
  2140     proof (cases rule: imethds_cases)
  2141       case NewMethod
  2142       with ifI hyp_newmethod
  2143       show ?thesis
  2144 	by auto
  2145     next
  2146       case (InheritedMethod J)
  2147       assume "J \<in> set (isuperIfs i)" 
  2148              "new \<in> imethds G J sig"
  2149       with hyp 
  2150       show "?thesis"
  2151 	by auto
  2152     qed
  2153   qed
  2154 qed
  2155 
  2156 text {*
  2157 Which dynamic classes are valid to look up a member of a distinct static type?
  2158 We have to distinct class members (named static members in Java) 
  2159 from instance members. Class members are global to all Objects of a class,
  2160 instance members are local to a single Object instance. If a member is
  2161 equipped with the static modifier it is a class member, else it is an 
  2162 instance member.
  2163 The following table gives an overview of the current framework. We assume
  2164 to have a reference with static type statT and a dynamic class dynC. Between
  2165 both of these types the widening relation holds 
  2166 @{term "G\<turnstile>Class dynC\<preceq> statT"}. Unfortunately this ordinary widening relation 
  2167 isn't enough to describe the valid lookup classes, since we must cope the
  2168 special cases of arrays and interfaces,too. If we statically expect an array or
  2169 inteface we may lookup a field or a method in Object which isn't covered in 
  2170 the widening relation.
  2171 \begin{verbatim}
  2172 statT      field         instance method       static (class) method
  2173 ------------------------------------------------------------------------
  2174  NullT      /                  /                   /
  2175  Iface      /                dynC                Object
  2176  Class    dynC               dynC                 dynC
  2177  Array      /                Object              Object
  2178 \end{verbatim}
  2179 In most cases we con lookup the member in the dynamic class. But as an
  2180 interface can't declare new static methods, nor an array can define new
  2181 methods at all, we have to lookup methods in the base class Object.
  2182 
  2183 The limitation to classes in the field column is artificial  and comes out
  2184 of the typing rule for the field access (see rule @{text "FVar"} in the 
  2185 welltyping relation @{term "wt"} in theory WellType). 
  2186 I stems out of the fact, that Object
  2187 indeed has no non private fields. So interfaces and arrays can actually
  2188 have no fields at all and a field access would be senseless. (In Java
  2189 interfaces are allowed to declare new fields but in current Bali not!).
  2190 So there is no principal reason why we should not allow Objects to declare
  2191 non private fields. Then we would get the following column:
  2192 \begin{verbatim}
  2193  statT    field
  2194 ----------------- 
  2195  NullT      /  
  2196  Iface    Object 
  2197  Class    dynC 
  2198  Array    Object
  2199 \end{verbatim}
  2200 *}
  2201 consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  2202                         ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
  2203 primrec
  2204 "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  2205 "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  2206               = (if static_membr 
  2207                     then dynC=Object 
  2208                     else G\<turnstile>Class dynC\<preceq> Iface I)"
  2209 "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  2210 "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  2211 
  2212 lemma valid_lookup_cls_is_class:
  2213  (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
  2214       ty_statT: "isrtype G statT" and
  2215             wf: "wf_prog G"
  2216  ) "is_class G dynC"
  2217 proof (cases statT)
  2218   case NullT
  2219   with dynC ty_statT show ?thesis
  2220     by (auto dest: widen_NT2)
  2221 next
  2222   case (IfaceT I)
  2223   with dynC wf show ?thesis
  2224     by (auto dest: implmt_is_class)
  2225 next
  2226   case (ClassT C)
  2227   with dynC ty_statT show ?thesis
  2228     by (auto dest: subcls_is_class2)
  2229 next
  2230   case (ArrayT T)
  2231   with dynC wf show ?thesis
  2232     by (auto)
  2233 qed
  2234 
  2235 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2236 ML_setup {*
  2237 simpset_ref() := simpset() delloop "split_all_tac";
  2238 claset_ref () := claset () delSWrapper "split_all_tac"
  2239 *}
  2240 
  2241 lemma dynamic_mheadsD:   
  2242 "\<lbrakk>emh \<in> mheads G S statT sig;    
  2243   G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
  2244   isrtype G statT; wf_prog G
  2245  \<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: 
  2246           is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh"
  2247 proof - 
  2248   assume      emh: "emh \<in> mheads G S statT sig"
  2249   and          wf: "wf_prog G"
  2250   and   dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)"
  2251   and      istype: "isrtype G statT"
  2252   from dynC_Prop istype wf 
  2253   obtain y where
  2254     dynC: "class G dynC = Some y" 
  2255     by (auto dest: valid_lookup_cls_is_class)
  2256   from emh wf show ?thesis
  2257   proof (cases rule: mheads_cases)
  2258     case Class_methd
  2259     fix statC statDeclC sm
  2260     assume     statC: "statT = ClassT statC"
  2261     assume            "accmethd G S statC sig = Some sm"
  2262     then have     sm: "methd G statC sig = Some sm" 
  2263       by (blast dest: accmethd_SomeD)  
  2264     assume eq_mheads: "mhead (mthd sm) = mhd emh"
  2265     from statC 
  2266     have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
  2267       by (simp add: dynlookup_def)
  2268     from wf statC istype dynC_Prop sm 
  2269     obtain dm where
  2270       "dynmethd G statC dynC sig = Some dm"
  2271       "is_static dm = is_static sm" 
  2272       "G\<turnstile>resTy dm\<preceq>resTy sm"  
  2273       by (auto dest!: ws_dynmethd accmethd_SomeD)
  2274     with dynlookup eq_mheads 
  2275     show ?thesis 
  2276       by (cases emh type: *) (auto)
  2277   next
  2278     case Iface_methd
  2279     fix I im
  2280     assume    statI: "statT = IfaceT I" and
  2281           eq_mheads: "mthd im = mhd emh" and
  2282                      "im \<in> accimethds G (pid S) I sig" 
  2283     then have im: "im \<in> imethds G I sig" 
  2284       by (blast dest: accimethdsD)
  2285     with istype statI eq_mheads wf 
  2286     have not_static_emh: "\<not> is_static emh"
  2287       by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2288     from statI im
  2289     have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2290       by (auto simp add: dynlookup_def dynimethd_def) 
  2291     from wf dynC_Prop statI istype im not_static_emh 
  2292     obtain dm where
  2293       "methd G dynC sig = Some dm"
  2294       "is_static dm = is_static im" 
  2295       "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2296       by (auto dest: implmt_methd)
  2297     with dynlookup eq_mheads
  2298     show ?thesis 
  2299       by (cases emh type: *) (auto)
  2300   next
  2301     case Iface_Object_methd
  2302     fix I sm
  2303     assume   statI: "statT = IfaceT I" and
  2304                 sm: "accmethd G S Object sig = Some sm" and 
  2305          eq_mheads: "mhead (mthd sm) = mhd emh" and
  2306              nPriv: "accmodi sm \<noteq> Private"
  2307      show ?thesis 
  2308      proof (cases "imethds G I sig = {}")
  2309        case True
  2310        with statI 
  2311        have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig"
  2312 	 by (simp add: dynlookup_def dynimethd_def)
  2313        from wf dynC 
  2314        have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2315 	 by (auto intro: subcls_ObjectI)
  2316        from wf dynC dynC_Prop istype sm subclsObj 
  2317        obtain dm where
  2318 	 "dynmethd G Object dynC sig = Some dm"
  2319 	 "is_static dm = is_static sm" 
  2320 	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)"  
  2321 	 by (auto dest!: ws_dynmethd accmethd_SomeD 
  2322                   intro: class_Object [OF wf])
  2323        with dynlookup eq_mheads
  2324        show ?thesis 
  2325 	 by (cases emh type: *) (auto)
  2326      next
  2327        case False
  2328        with statI
  2329        have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2330 	 by (simp add: dynlookup_def dynimethd_def)
  2331        from istype statI
  2332        have "is_iface G I"
  2333 	 by auto
  2334        with wf sm nPriv False 
  2335        obtain im where
  2336 	      im: "im \<in> imethds G I sig" and
  2337 	 eq_stat: "is_static im = is_static sm" and
  2338          resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)"
  2339 	 by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD)
  2340        from im wf statI istype eq_stat eq_mheads
  2341        have not_static_sm: "\<not> is_static emh"
  2342 	 by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2343        from im wf dynC_Prop dynC istype statI not_static_sm
  2344        obtain dm where
  2345 	 "methd G dynC sig = Some dm"
  2346 	 "is_static dm = is_static im" 
  2347 	 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2348 	 by (auto dest: implmt_methd)
  2349        with wf eq_stat resProp dynlookup eq_mheads
  2350        show ?thesis 
  2351 	 by (cases emh type: *) (auto intro: widen_trans)
  2352      qed
  2353   next
  2354     case Array_Object_methd
  2355     fix T sm
  2356     assume statArr: "statT = ArrayT T" and
  2357                 sm: "accmethd G S Object sig = Some sm" and 
  2358          eq_mheads: "mhead (mthd sm) = mhd emh" 
  2359     from statArr dynC_Prop wf
  2360     have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
  2361       by (auto simp add: dynlookup_def dynmethd_C_C)
  2362     with sm eq_mheads sm 
  2363     show ?thesis 
  2364       by (cases emh type: *) (auto dest: accmethd_SomeD)
  2365   qed
  2366 qed
  2367 
  2368 (* Tactical version *)
  2369 (*
  2370 lemma dynamic_mheadsD: "  
  2371  \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y;  
  2372    if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; 
  2373    isrtype G statT\<rbrakk> \<Longrightarrow>  
  2374   \<exists>m \<in> dynlookup G statT dynC sig: 
  2375      static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)"
  2376 apply (drule mheadsD)
  2377 apply safe
  2378        -- reftype statT is a class  
  2379 apply  (case_tac "\<exists>T. ClassT C = ArrayT T")
  2380 apply    (simp)
  2381 
  2382 apply    (clarsimp simp add: dynlookup_def )
  2383 apply    (frule_tac statC="C" and dynC="dynC"  and sig="sig"  
  2384          in ws_dynmethd)
  2385 apply      assumption+
  2386 apply    (case_tac "emh")  
  2387 apply    (force dest: accmethd_SomeD)
  2388 
  2389        -- reftype statT is a interface, method defined in interface 
  2390 apply    (clarsimp simp add: dynlookup_def)
  2391 apply    (drule (1) implmt_methd)
  2392 apply      blast
  2393 apply      blast
  2394 apply    (clarify)  
  2395 apply    (unfold dynimethd_def)
  2396 apply    (rule_tac x="cm" in bexI)
  2397 apply      (case_tac "emh")
  2398 apply      force
  2399 
  2400 apply      force
  2401 
  2402         -- reftype statT is a interface, method defined in Object 
  2403 apply    (simp add: dynlookup_def)
  2404 apply    (simp only: dynimethd_def)
  2405 apply    (case_tac "imethds G I sig = {}")
  2406 apply       simp
  2407 apply       (frule_tac statC="Object" and dynC="dynC"  and sig="sig"  
  2408              in ws_dynmethd)
  2409 apply          (blast intro: subcls_ObjectI wf_ws_prog) 
  2410 apply          (blast dest: class_Object)
  2411 apply       (case_tac "emh") 
  2412 apply       (force dest: accmethd_SomeD)
  2413 
  2414 apply       simp
  2415 apply       (subgoal_tac "\<exists> im. im \<in> imethds G I sig") 
  2416 prefer 2      apply blast
  2417 apply       clarify
  2418 apply       (frule (1) implmt_methd)
  2419 apply         simp
  2420 apply         blast  
  2421 apply       (clarify dest!: accmethd_SomeD)
  2422 apply       (frule (4) iface_overrides_Object)
  2423 apply       clarify
  2424 apply       (case_tac emh)
  2425 apply       force
  2426 
  2427         -- reftype statT is a array
  2428 apply    (simp add: dynlookup_def)
  2429 apply    (case_tac emh)
  2430 apply    (force dest: accmethd_SomeD simp add: dynmethd_def)
  2431 done
  2432 *)
  2433 
  2434 (* ### auf ws_class_induct umstellen *)
  2435 lemma methd_declclass:
  2436 "\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> 
  2437  \<Longrightarrow> methd G (declclass m) sig = Some m"
  2438 proof -
  2439   assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m"
  2440   have "wf_prog G  \<longrightarrow> 
  2441 	   (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
  2442                    \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
  2443   proof (rule class_rec.induct,intro allI impI)
  2444     fix G C c m
  2445     assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
  2446                      ?P G (super c)"
  2447     assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  2448             m: "methd G C sig = Some m"
  2449     show "methd G (declclass m) sig = Some m"
  2450     proof (cases "C=Object")
  2451       case True
  2452       with wf m show ?thesis by (auto intro: table_of_map_SomeI)
  2453     next
  2454       let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  2455       let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  2456       case False
  2457       with cls_C wf m
  2458       have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  2459 	by (simp add: methd_rec)
  2460       show ?thesis
  2461       proof (cases "?table sig")
  2462 	case None
  2463 	from this methd_C have "?filter (methd G (super c)) sig = Some m"
  2464 	  by simp
  2465 	moreover
  2466 	from wf cls_C False obtain sup where "class G (super c) = Some sup"
  2467 	  by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  2468 	moreover note wf False cls_C hyp
  2469 	ultimately show ?thesis by auto
  2470       next
  2471 	case Some
  2472 	from this methd_C m show ?thesis by auto 
  2473       qed
  2474     qed
  2475   qed	
  2476   with asm show ?thesis by auto
  2477 qed
  2478 
  2479 lemma dynmethd_declclass:
  2480  "\<lbrakk>dynmethd G statC dynC sig = Some m;
  2481    wf_prog G; is_class G statC
  2482   \<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m"
  2483 by (auto dest: dynmethd_declC)
  2484 
  2485 lemma dynlookup_declC:
  2486  "\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G;
  2487    is_class G dynC;isrtype G statT
  2488   \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)"
  2489 by (cases "statT")
  2490    (auto simp add: dynlookup_def dynimethd_def 
  2491              dest: methd_declC dynmethd_declC)
  2492 
  2493 lemma dynlookup_Array_declclassD [simp]:
  2494 "\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> 
  2495  \<Longrightarrow> declclass dm = Object"
  2496 proof -
  2497   assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm"
  2498   assume wf: "wf_prog G"
  2499   from wf have ws: "ws_prog G" by auto
  2500   from wf have is_cls_Obj: "is_class G Object" by auto
  2501   from dynL wf
  2502   show ?thesis
  2503     by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws]
  2504                  dest: methd_Object_SomeD)
  2505 qed   
  2506   
  2507 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2508 ML_setup {*
  2509 simpset_ref() := simpset() delloop "split_all_tac";
  2510 claset_ref () := claset () delSWrapper "split_all_tac"
  2511 *}
  2512 
  2513 lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
  2514   dt=empty_dt \<longrightarrow> (case T of 
  2515                      Inl T \<Rightarrow> is_type (prg E) T 
  2516                    | Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))"
  2517 apply (unfold empty_dt_def)
  2518 apply (erule wt.induct)
  2519 apply (auto split del: split_if_asm simp del: snd_conv 
  2520             simp add: is_acc_class_def is_acc_type_def)
  2521 apply    (erule typeof_empty_is_type)
  2522 apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1, 
  2523         force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
  2524 apply  (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
  2525 apply  (drule_tac [2] accfield_fields) 
  2526 apply  (frule class_Object)
  2527 apply  (auto dest: accmethd_rT_is_type 
  2528                    imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type]
  2529              dest!:accimethdsD
  2530              simp del: class_Object
  2531              simp add: is_acc_type_def
  2532     )
  2533 done
  2534 declare split_paired_All [simp] split_paired_Ex [simp]
  2535 ML_setup {*
  2536 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
  2537 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  2538 *}
  2539 
  2540 lemma ty_expr_is_type: 
  2541 "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2542 by (auto dest!: wt_is_type)
  2543 lemma ty_var_is_type: 
  2544 "\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2545 by (auto dest!: wt_is_type)
  2546 lemma ty_exprs_is_type: 
  2547 "\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))"
  2548 by (auto dest!: wt_is_type)
  2549 
  2550 
  2551 lemma static_mheadsD: 
  2552  "\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; 
  2553    invmode (mhd emh) e \<noteq> IntVir 
  2554   \<rbrakk> \<Longrightarrow> \<exists>m. (   (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m)
  2555                \<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> 
  2556           declrefT emh = ClassT (declclass m) \<and>  mhead (mthd m) = (mhd emh)"
  2557 apply (subgoal_tac "is_static emh \<or> e = Super")
  2558 defer apply (force simp add: invmode_def)
  2559 apply (frule  ty_expr_is_type)
  2560 apply   simp
  2561 apply (case_tac "is_static emh")
  2562 apply  (frule (1) mheadsD)
  2563 apply  clarsimp
  2564 apply  safe
  2565 apply    blast
  2566 apply   (auto dest!: imethds_wf_mhead
  2567                      accmethd_SomeD 
  2568                      accimethdsD
  2569               simp add: accObjectmheads_def Objectmheads_def)
  2570 
  2571 apply  (erule wt_elim_cases)
  2572 apply  (force simp add: cmheads_def)
  2573 done
  2574 
  2575 lemma wt_MethdI:  
  2576 "\<lbrakk>methd G C sig = Some m; wf_prog G;  
  2577   class G C = Some c\<rbrakk> \<Longrightarrow>  
  2578  \<exists>T. \<lparr>prg=G,cls=(declclass m),
  2579       lcl=\<lambda> k. 
  2580           (case k of
  2581              EName e 
  2582              \<Rightarrow> (case e of 
  2583                    VNam v 
  2584                    \<Rightarrow> (table_of (lcls (mbody (mthd m)))
  2585                                 ((pars (mthd m))[\<mapsto>](parTs sig))) v
  2586                  | Res \<Rightarrow> Some (resTy (mthd m)))
  2587            | This \<Rightarrow> if is_static m then None else Some (Class (declclass m)))
  2588      \<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
  2589 apply (frule (2) methd_wf_mdecl, clarify)
  2590 apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
  2591 done
  2592 
  2593 subsection "accessibility concerns"
  2594 
  2595 lemma mheads_type_accessible:
  2596  "\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk>
  2597  \<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)"
  2598 by (erule mheads_cases)
  2599    (auto dest: accmethd_SomeD accessible_from_commonD accimethdsD)
  2600 
  2601 lemma static_to_dynamic_accessible_from:
  2602 "\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> 
  2603  \<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC"
  2604 proof (induct rule: accessible_fromR.induct)
  2605 qed (auto intro: dyn_accessible_fromR.intros 
  2606                  member_of_to_member_in
  2607                  static_to_dynamic_overriding)
  2608 
  2609 lemma static_to_dynamic_accessible_from:
  2610  (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  2611           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2612                 wf: "wf_prog G"
  2613  ) "G\<turnstile>m in dynC dyn_accessible_from accC"
  2614 proof - 
  2615   from stat_acc subclseq 
  2616   show ?thesis (is "?Dyn_accessible m")
  2617   proof (induct rule: accessible_fromR.induct)
  2618     case (immediate statC m)
  2619     then show "?Dyn_accessible m"
  2620       by (blast intro: dyn_accessible_fromR.immediate
  2621                        member_inI
  2622                        permits_acc_inheritance)
  2623   next
  2624     case (overriding _ _ m)
  2625     with wf show "?Dyn_accessible m"
  2626       by (blast intro: dyn_accessible_fromR.overriding
  2627                        member_inI
  2628                        static_to_dynamic_overriding  
  2629                        rtrancl_trancl_trancl 
  2630                        static_to_dynamic_accessible_from)
  2631   qed
  2632 qed
  2633 
  2634 lemma dynmethd_member_in:
  2635  (assumes    m: "dynmethd G statC dynC sig = Some m" and
  2636    iscls_statC: "is_class G statC" and
  2637             wf: "wf_prog G"
  2638  ) "G\<turnstile>Methd sig m member_in dynC"
  2639 proof -
  2640   from m 
  2641   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2642     by (auto simp add: dynmethd_def)
  2643   from subclseq iscls_statC 
  2644   have iscls_dynC: "is_class G dynC"
  2645     by (rule subcls_is_class2)
  2646   from  iscls_dynC iscls_statC wf m
  2647   have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and>
  2648         methd G (declclass m) sig = Some m" 
  2649     by - (drule dynmethd_declC, auto)
  2650   with wf 
  2651   show ?thesis
  2652     by (auto intro: member_inI dest: methd_member_of)
  2653 qed
  2654 
  2655 lemma dynmethd_access_prop:
  2656   (assumes statM: "methd G statC sig = Some statM" and
  2657         stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
  2658             dynM: "dynmethd G statC dynC sig = Some dynM" and
  2659               wf: "wf_prog G" 
  2660    ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2661 proof -
  2662   from wf have ws: "ws_prog G" ..
  2663   from dynM 
  2664   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2665     by (auto simp add: dynmethd_def)
  2666   from stat_acc 
  2667   have is_cls_statC: "is_class G statC"
  2668     by (auto dest: accessible_from_commonD member_of_is_classD)
  2669   with subclseq 
  2670   have is_cls_dynC: "is_class G dynC"
  2671     by (rule subcls_is_class2)
  2672   from is_cls_statC statM wf 
  2673   have member_statC: "G\<turnstile>Methd sig statM member_of statC"
  2674     by (auto intro: methd_member_of)
  2675   from stat_acc 
  2676   have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)"
  2677     by (auto dest: accessible_from_commonD)
  2678   from statM subclseq is_cls_statC ws 
  2679   show ?thesis
  2680   proof (cases rule: dynmethd_cases)
  2681     case Static
  2682     assume dynmethd: "dynmethd G statC dynC sig = Some statM"
  2683     with dynM have eq_dynM_statM: "dynM=statM" 
  2684       by simp
  2685     with stat_acc subclseq wf 
  2686     show ?thesis
  2687       by (auto intro: static_to_dynamic_accessible_from)
  2688   next
  2689     case (Overrides newM)
  2690     assume dynmethd: "dynmethd G statC dynC sig = Some newM"
  2691     assume override: "G,sig\<turnstile>newM overrides statM"
  2692     assume      neq: "newM\<noteq>statM"
  2693     from dynmethd dynM 
  2694     have eq_dynM_newM: "dynM=newM" 
  2695       by simp
  2696     from dynmethd eq_dynM_newM wf is_cls_statC
  2697     have "G\<turnstile>Methd sig dynM member_in dynC"
  2698       by (auto intro: dynmethd_member_in)
  2699     moreover
  2700     from subclseq
  2701     have "G\<turnstile>dynC\<prec>\<^sub>C statC"
  2702     proof (cases rule: subclseq_cases)
  2703       case Eq
  2704       assume "dynC=statC"
  2705       moreover
  2706       from is_cls_statC obtain c
  2707 	where "class G statC = Some c"
  2708 	by auto
  2709       moreover 
  2710       note statM ws dynmethd 
  2711       ultimately
  2712       have "newM=statM" 
  2713 	by (auto simp add: dynmethd_C_C)
  2714       with neq show ?thesis 
  2715 	by (contradiction)
  2716     next
  2717       case Subcls show ?thesis .
  2718     qed 
  2719     moreover
  2720     from stat_acc wf 
  2721     have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC"
  2722       by (blast intro: static_to_dynamic_accessible_from)
  2723     moreover
  2724     note override eq_dynM_newM
  2725     ultimately show ?thesis
  2726       by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.overriding)
  2727   qed
  2728 qed
  2729 
  2730 lemma implmt_methd_access:
  2731 (fixes accC::qtname
  2732  assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2733            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2734                isif_I: "is_iface G I" and
  2735                    wf: "wf_prog G" 
  2736  ) "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
  2737             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2738 proof -
  2739   from implements 
  2740   have iscls_dynC: "is_class G dynC" by (rule implmt_is_class)
  2741   from iface_methd
  2742   obtain im
  2743     where "im \<in> imethds G I sig"
  2744     by auto
  2745   with wf implements isif_I 
  2746   obtain dynM 
  2747     where dynM: "methd G dynC sig = Some dynM" and
  2748            pub: "accmodi dynM = Public"
  2749     by (blast dest: implmt_methd)
  2750   with iscls_dynC wf
  2751   have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2752     by (auto intro!: dyn_accessible_fromR.immediate 
  2753               intro: methd_member_of member_of_to_member_in
  2754                      simp add: permits_acc_def)
  2755   with dynM    
  2756   show ?thesis
  2757     by blast
  2758 qed
  2759 
  2760 corollary implmt_dynimethd_access:
  2761 (fixes accC::qtname
  2762  assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2763            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2764                isif_I: "is_iface G I" and
  2765                    wf: "wf_prog G" 
  2766  ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
  2767             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2768 proof -
  2769   from iface_methd
  2770   have "dynimethd G I dynC sig = methd G dynC sig"
  2771     by (simp add: dynimethd_def)
  2772   with iface_methd implements isif_I wf 
  2773   show ?thesis
  2774     by (simp only:)
  2775        (blast intro: implmt_methd_access)
  2776 qed
  2777 
  2778 lemma dynlookup_access_prop:
  2779  (assumes emh: "emh \<in> mheads G accC statT sig" and
  2780          dynM: "dynlookup G statT dynC sig = Some dynM" and
  2781     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
  2782     isT_statT: "isrtype G statT" and
  2783            wf: "wf_prog G"
  2784  ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2785 proof -
  2786   from emh wf
  2787   have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
  2788     by (rule mheads_type_accessible)
  2789   from dynC_prop isT_statT wf
  2790   have iscls_dynC: "is_class G dynC"
  2791     by (rule valid_lookup_cls_is_class)
  2792   from emh dynC_prop isT_statT wf dynM
  2793   have eq_static: "is_static emh = is_static dynM"
  2794     by (auto dest: dynamic_mheadsD)
  2795   from emh wf show ?thesis
  2796   proof (cases rule: mheads_cases)
  2797     case (Class_methd statC _ statM)
  2798     assume statT: "statT = ClassT statC"
  2799     assume "accmethd G accC statC sig = Some statM"
  2800     then have    statM: "methd G statC sig = Some statM" and
  2801               stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC"
  2802       by (auto dest: accmethd_SomeD)
  2803     from dynM statT
  2804     have dynM': "dynmethd G statC dynC sig = Some dynM"
  2805       by (simp add: dynlookup_def) 
  2806     from statM stat_acc wf dynM'
  2807     show ?thesis
  2808       by (auto dest!: dynmethd_access_prop)
  2809   next
  2810     case (Iface_methd I im)
  2811     then have iface_methd: "imethds G I sig \<noteq> {}" and
  2812                  statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 
  2813       by (auto dest: accimethdsD)
  2814     assume   statT: "statT = IfaceT I"
  2815     assume      im: "im \<in>  accimethds G (pid accC) I sig"
  2816     assume eq_mhds: "mthd im = mhd emh"
  2817     from dynM statT
  2818     have dynM': "dynimethd G I dynC sig = Some dynM"
  2819       by (simp add: dynlookup_def)
  2820     from isT_statT statT 
  2821     have isif_I: "is_iface G I"
  2822       by simp
  2823     show ?thesis
  2824     proof (cases "is_static emh")
  2825       case False
  2826       with statT dynC_prop 
  2827       have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT"
  2828 	by simp
  2829       from statT widen_dynC
  2830       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2831 	by auto    
  2832       from eq_static False 
  2833       have not_static_dynM: "\<not> is_static dynM" 
  2834 	by simp
  2835       from iface_methd implmnt isif_I wf dynM'
  2836       show ?thesis
  2837 	by - (drule implmt_dynimethd_access, auto)
  2838     next
  2839       case True
  2840       assume "is_static emh"
  2841       moreover
  2842       from wf isT_statT statT im 
  2843       have "\<not> is_static im"
  2844 	by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead)
  2845       moreover note eq_mhds
  2846       ultimately show ?thesis
  2847 	by (cases emh) auto
  2848     qed
  2849   next
  2850     case (Iface_Object_methd I statM)
  2851     assume statT: "statT = IfaceT I"
  2852     assume "accmethd G accC Object sig = Some statM"
  2853     then have    statM: "methd G Object sig = Some statM" and
  2854               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2855       by (auto dest: accmethd_SomeD)
  2856     assume not_Private_statM: "accmodi statM \<noteq> Private"
  2857     assume eq_mhds: "mhead (mthd statM) = mhd emh"
  2858     from iscls_dynC wf
  2859     have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2860       by (auto intro: subcls_ObjectI)
  2861     show ?thesis
  2862     proof (cases "imethds G I sig = {}")
  2863       case True
  2864       from dynM statT True
  2865       have dynM': "dynmethd G Object dynC sig = Some dynM"
  2866 	by (simp add: dynlookup_def dynimethd_def)
  2867       from statT  
  2868       have "G\<turnstile>RefT statT \<preceq>Class Object"
  2869 	by auto
  2870       with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT 
  2871         wf dynM' eq_static dynC_prop  
  2872       show ?thesis
  2873 	by - (drule dynmethd_access_prop,force+) 
  2874     next
  2875       case False
  2876       then obtain im where
  2877 	im: "im \<in>  imethds G I sig"
  2878 	by auto
  2879       have not_static_emh: "\<not> is_static emh"
  2880       proof -
  2881 	from im statM statT isT_statT wf not_Private_statM 
  2882 	have "is_static im = is_static statM"
  2883 	  by (auto dest: wf_imethds_hiding_objmethdsD)
  2884 	with wf isT_statT statT im 
  2885 	have "\<not> is_static statM"
  2886 	  by (auto dest: wf_prog_idecl imethds_wf_mhead)
  2887 	with eq_mhds
  2888 	show ?thesis  
  2889 	  by (cases emh) auto
  2890       qed
  2891       with statT dynC_prop
  2892       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2893 	by simp
  2894       with isT_statT statT
  2895       have isif_I: "is_iface G I"
  2896 	by simp
  2897       from dynM statT
  2898       have dynM': "dynimethd G I dynC sig = Some dynM"
  2899 	by (simp add: dynlookup_def) 
  2900       from False implmnt isif_I wf dynM'
  2901       show ?thesis
  2902 	by - (drule implmt_dynimethd_access, auto)
  2903     qed
  2904   next
  2905     case (Array_Object_methd T statM)
  2906     assume statT: "statT = ArrayT T"
  2907     assume "accmethd G accC Object sig = Some statM"
  2908     then have    statM: "methd G Object sig = Some statM" and
  2909               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2910       by (auto dest: accmethd_SomeD)
  2911     from statT dynC_prop
  2912     have dynC_Obj: "dynC = Object" 
  2913       by simp
  2914     then
  2915     have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object"
  2916       by simp
  2917     from dynM statT    
  2918     have dynM': "dynmethd G Object dynC sig = Some dynM"
  2919       by (simp add: dynlookup_def)
  2920     from statM statT_acc stat_acc dynM' wf widen_dynC_Obj  
  2921          statT isT_statT  
  2922     show ?thesis   
  2923       by - (drule dynmethd_access_prop, simp+) 
  2924   qed
  2925 qed
  2926 
  2927 lemma dynlookup_access:
  2928  (assumes emh: "emh \<in> mheads G accC statT sig" and
  2929     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
  2930     isT_statT: "isrtype G statT" and
  2931            wf: "wf_prog G"
  2932  ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
  2933             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2934 proof - 
  2935   from dynC_prop isT_statT wf
  2936   have is_cls_dynC: "is_class G dynC"
  2937     by (auto dest: valid_lookup_cls_is_class)
  2938   with emh wf dynC_prop isT_statT
  2939   obtain dynM where 
  2940     "dynlookup G statT dynC sig = Some dynM"
  2941     by - (drule dynamic_mheadsD,auto)
  2942   with  emh dynC_prop isT_statT wf
  2943   show ?thesis 
  2944     by (blast intro: dynlookup_access_prop)
  2945 qed
  2946 
  2947 lemma stat_overrides_Package_old: 
  2948 (assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
  2949           accmodi_new: "accmodi new = Package" and
  2950                    wf: "wf_prog G "
  2951 ) "accmodi old = Package"
  2952 proof -
  2953   from stat_override wf 
  2954   have "accmodi old \<le> accmodi new"
  2955     by (auto dest: wf_prog_stat_overridesD)
  2956   with stat_override accmodi_new show ?thesis
  2957     by (cases "accmodi old") (auto dest: no_Private_stat_override 
  2958                                    dest: acc_modi_le_Dests)
  2959 qed
  2960 
  2961 text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
  2962 Without it. it is easy to leaf the Package!
  2963 *}
  2964 lemma dyn_accessible_Package:
  2965  "\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package;
  2966    wf_prog G\<rbrakk>
  2967   \<Longrightarrow> pid accC = pid (declclass m)"
  2968 proof -
  2969   assume wf: "wf_prog G "
  2970   assume accessible: "G \<turnstile> m in C dyn_accessible_from accC"
  2971   then show "accmodi m = Package 
  2972             \<Longrightarrow> pid accC = pid (declclass m)"
  2973     (is "?Pack m \<Longrightarrow> ?P m")
  2974   proof (induct rule: dyn_accessible_fromR.induct)
  2975     case (immediate C m)
  2976     assume "G\<turnstile>m member_in C"
  2977            "G \<turnstile> m in C permits_acc_to accC"
  2978            "accmodi m = Package"      
  2979     then show "?P m"
  2980       by (auto simp add: permits_acc_def)
  2981   next
  2982     case (overriding declC C new newm old Sup)
  2983     assume member_new: "G \<turnstile> new member_in C" and
  2984                   new: "new = (declC, mdecl newm)" and
  2985              override: "G \<turnstile> (declC, newm) overrides old" and
  2986          subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
  2987               acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and
  2988                   hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and
  2989           accmodi_new: "accmodi new = Package"
  2990     from override accmodi_new new wf 
  2991     have accmodi_old: "accmodi old = Package"  
  2992       by (auto dest: overrides_Package_old)
  2993     with hyp 
  2994     have P_sup: "?P (methdMembr old)"
  2995       by (simp)
  2996     from wf override new accmodi_old accmodi_new
  2997     have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
  2998       by (auto dest: dyn_override_Package)
  2999     with eq_pid_new_old P_sup show "?P new"
  3000       by auto
  3001   qed
  3002 qed
  3003 
  3004 end