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