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