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