src/HOL/Bali/WellForm.thy
author nipkow
Mon Sep 12 07:55:43 2011 +0200 (2011-09-12)
changeset 44890 22f665a2e91c
parent 37956 ee939247b2fb
child 45605 a89b4bc311a5
permissions -rw-r--r--
new fastforce replacing fastsimp - less confusing name
     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                             \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
    62                             is_acc_type G P (resTy mh) \<and>
    63                             \<spacespace> 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 lemma wf_imethdsD: 
   737  "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
   738  \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
   739 proof -
   740   assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
   741 
   742   note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
   743   have "wf_prog G \<longrightarrow> 
   744          (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
   745                   \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
   746   proof (induct G I rule: iface_rec_induct', intro allI impI)
   747     fix G I i im
   748     assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i)
   749                  \<Longrightarrow> ?P G J"
   750     assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
   751            im: "im \<in> imethds G I sig" 
   752     show "\<not>is_static im \<and> accmodi im = Public" 
   753     proof -
   754       let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
   755       let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
   756       from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
   757         by (simp add: imethds_rec)
   758       from wf if_I have 
   759         wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)"
   760         by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
   761       from wf if_I have
   762         "\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public"
   763         by (auto dest!: wf_prog_idecl wf_idecl_mhead)
   764       then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
   765                          \<longrightarrow>  \<not> is_static im \<and> accmodi im = Public"
   766         by (auto dest!: table_of_Some_in_set)
   767       show ?thesis
   768         proof (cases "?new sig = {}")
   769           case True
   770           from True wf wf_supI if_I imethds hyp 
   771           show ?thesis by (auto simp del:  split_paired_All)  
   772         next
   773           case False
   774           from False wf wf_supI if_I imethds new_ok hyp 
   775           show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
   776         qed
   777       qed
   778     qed
   779   with asm show ?thesis by (auto simp del: split_paired_All)
   780 qed
   781 
   782 lemma wf_prog_hidesD:
   783   assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G"
   784   shows
   785    "accmodi old \<le> accmodi new \<and>
   786     is_static old"
   787 proof -
   788   from hides 
   789   obtain c where 
   790     clsNew: "class G (declclass new) = Some c" and
   791     neqObj: "declclass new \<noteq> Object"
   792     by (auto dest: hidesD declared_in_classD)
   793   with hides obtain newM oldM where
   794     newM: "table_of (methods c) (msig new) = Some newM" and 
   795      new: "new = (declclass new,(msig new),newM)" and
   796      old: "old = (declclass old,(msig old),oldM)" and
   797           "msig new = msig old"
   798     by (cases new,cases old) 
   799        (auto dest: hidesD 
   800          simp add: cdeclaredmethd_def declared_in_def)
   801   with hides 
   802   have hides':
   803         "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)"
   804     by auto
   805   from clsNew wf 
   806   have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   807   note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
   808   with new old 
   809   show ?thesis
   810     by (cases new, cases old) auto
   811 qed
   812 
   813 text {* Compare this lemma about static  
   814 overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 
   815 dynamic overriding @{term "G \<turnstile>new overrides old"}. 
   816 Conforming result types and restrictions on the access modifiers of the old 
   817 and the new method are not part of the predicate for static overriding. But
   818 they are enshured in a wellfromed program.  Dynamic overriding has 
   819 no restrictions on the access modifiers but enforces confrom result types 
   820 as precondition. But with some efford we can guarantee the access modifier
   821 restriction for dynamic overriding, too. See lemma 
   822 @{text wf_prog_dyn_override_prop}.
   823 *}
   824 lemma wf_prog_stat_overridesD:
   825   assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
   826   shows
   827    "G\<turnstile>resTy new\<preceq>resTy old \<and>
   828     accmodi old \<le> accmodi new \<and>
   829     \<not> is_static old"
   830 proof -
   831   from stat_override 
   832   obtain c where 
   833     clsNew: "class G (declclass new) = Some c" and
   834     neqObj: "declclass new \<noteq> Object"
   835     by (auto dest: stat_overrides_commonD declared_in_classD)
   836   with stat_override obtain newM oldM where
   837     newM: "table_of (methods c) (msig new) = Some newM" and 
   838      new: "new = (declclass new,(msig new),newM)" and
   839      old: "old = (declclass old,(msig old),oldM)" and
   840           "msig new = msig old"
   841     by (cases new,cases old) 
   842        (auto dest: stat_overrides_commonD 
   843          simp add: cdeclaredmethd_def declared_in_def)
   844   with stat_override 
   845   have stat_override':
   846         "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
   847     by auto
   848   from clsNew wf 
   849   have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
   850   note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
   851   with new old 
   852   show ?thesis
   853     by (cases new, cases old) auto
   854 qed
   855     
   856 lemma static_to_dynamic_overriding: 
   857   assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G"
   858   shows "G\<turnstile>new overrides old"
   859 proof -
   860   from stat_override 
   861   show ?thesis (is "?Overrides new old")
   862   proof (induct)
   863     case (Direct new old superNew)
   864     then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 
   865       by (rule stat_overridesR.Direct)
   866     from stat_override wf
   867     have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and
   868       not_static_old: "\<not> is_static old" 
   869       by (auto dest: wf_prog_stat_overridesD)  
   870     have not_private_new: "accmodi new \<noteq> Private"
   871     proof -
   872       from stat_override 
   873       have "accmodi old \<noteq> Private"
   874         by (rule no_Private_stat_override)
   875       moreover
   876       from stat_override wf
   877       have "accmodi old \<le> accmodi new"
   878         by (auto dest: wf_prog_stat_overridesD)
   879       ultimately
   880       show ?thesis
   881         by (auto dest: acc_modi_bottom)
   882     qed
   883     with Direct resTy_widen not_static_old 
   884     show "?Overrides new old" 
   885       by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
   886   next
   887     case (Indirect new inter old)
   888     then show "?Overrides new old" 
   889       by (blast intro: overridesR.Indirect) 
   890   qed
   891 qed
   892 
   893 lemma non_Package_instance_method_inheritance:
   894   assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
   895               accmodi_old: "accmodi old \<noteq> Package" and 
   896           instance_method: "\<not> is_static old" and
   897                    subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
   898              old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
   899                        wf: "wf_prog G"
   900   shows "G\<turnstile>Method old member_of C \<or>
   901    (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
   902 proof -
   903   from wf have ws: "ws_prog G" by auto
   904   from old_declared have iscls_declC_old: "is_class G (declclass old)"
   905     by (auto simp add: declared_in_def cdeclaredmethd_def)
   906   from subcls have  iscls_C: "is_class G C"
   907     by (blast dest:  subcls_is_class)
   908   from iscls_C ws old_inheritable subcls 
   909   show ?thesis (is "?P C old")
   910   proof (induct rule: ws_class_induct')
   911     case Object
   912     assume "G\<turnstile>Object\<prec>\<^sub>C declclass old"
   913     then show "?P Object old"
   914       by blast
   915   next
   916     case (Subcls C c)
   917     assume cls_C: "class G C = Some c" and 
   918        neq_C_Obj: "C \<noteq> Object" and
   919              hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 
   920                    G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and
   921      inheritable: "G \<turnstile>Method old inheritable_in pid C" and
   922          subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
   923     from cls_C neq_C_Obj  
   924     have super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 
   925       by (rule subcls1I)
   926     from wf cls_C neq_C_Obj
   927     have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
   928       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
   929     {
   930       fix old
   931       assume    member_super: "G\<turnstile>Method old member_of (super c)"
   932       assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
   933       assume instance_method: "\<not> is_static old"
   934       from member_super
   935       have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
   936        by (cases old) (auto dest: member_of_declC)
   937       have "?P C old"
   938       proof (cases "G\<turnstile>mid (msig old) undeclared_in C")
   939         case True
   940         with inheritable super accessible_super member_super
   941         have "G\<turnstile>Method old member_of C"
   942           by (cases old) (auto intro: members.Inherited)
   943         then show ?thesis
   944           by auto
   945       next
   946         case False
   947         then obtain new_member where
   948              "G\<turnstile>new_member declared_in C" and
   949              "mid (msig old) = memberid new_member"
   950           by (auto dest: not_undeclared_declared)
   951         then obtain new where
   952                   new: "G\<turnstile>Method new declared_in C" and
   953                eq_sig: "msig old = msig new" and
   954             declC_new: "declclass new = C" 
   955           by (cases new_member) auto
   956         then have member_new: "G\<turnstile>Method new member_of C"
   957           by (cases new) (auto intro: members.Immediate)
   958         from declC_new super member_super
   959         have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
   960           by (auto dest!: member_of_subclseq_declC
   961                     dest: r_into_trancl intro: trancl_rtrancl_trancl)
   962         show ?thesis
   963         proof (cases "is_static new")
   964           case False
   965           with eq_sig declC_new new old_declared inheritable
   966                super member_super subcls_new_old
   967           have "G\<turnstile>new overrides\<^sub>S old"
   968             by (auto intro!: stat_overridesR.Direct)
   969           with member_new show ?thesis
   970             by blast
   971         next
   972           case True
   973           with eq_sig declC_new subcls_new_old new old_declared inheritable
   974           have "G\<turnstile>new hides old"
   975             by (auto intro: hidesI)    
   976           with wf 
   977           have "is_static old"
   978             by (blast dest: wf_prog_hidesD)
   979           with instance_method
   980           show ?thesis
   981             by (contradiction)
   982         qed
   983       qed
   984     } note hyp_member_super = this
   985     from subclsC cls_C 
   986     have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
   987       by (rule subcls_superD)
   988     then
   989     show "?P C old"
   990     proof (cases rule: subclseq_cases) 
   991       case Eq
   992       assume "super c = declclass old"
   993       with old_declared 
   994       have "G\<turnstile>Method old member_of (super c)" 
   995         by (cases old) (auto intro: members.Immediate)
   996       with inheritable instance_method 
   997       show ?thesis
   998         by (blast dest: hyp_member_super)
   999     next
  1000       case Subcls
  1001       assume "G\<turnstile>super c\<prec>\<^sub>C declclass old"
  1002       moreover
  1003       from inheritable accmodi_old
  1004       have "G \<turnstile>Method old inheritable_in pid (super c)"
  1005         by (cases "accmodi old") (auto simp add: inheritable_in_def)
  1006       ultimately
  1007       have "?P (super c) old"
  1008         by (blast dest: hyp)
  1009       then show ?thesis
  1010       proof
  1011         assume "G \<turnstile>Method old member_of super c"
  1012         with inheritable instance_method
  1013         show ?thesis
  1014           by (blast dest: hyp_member_super)
  1015       next
  1016         assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c"
  1017         then obtain super_new where
  1018           super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
  1019             super_new_member:  "G \<turnstile>Method super_new member_of super c"
  1020           by blast
  1021         from super_new_override wf
  1022         have "accmodi old \<le> accmodi super_new"
  1023           by (auto dest: wf_prog_stat_overridesD)
  1024         with inheritable accmodi_old
  1025         have "G \<turnstile>Method super_new inheritable_in pid C"
  1026           by (auto simp add: inheritable_in_def 
  1027                       split: acc_modi.splits
  1028                        dest: acc_modi_le_Dests)
  1029         moreover
  1030         from super_new_override 
  1031         have "\<not> is_static super_new"
  1032           by (auto dest: stat_overrides_commonD)
  1033         moreover
  1034         note super_new_member
  1035         ultimately have "?P C super_new"
  1036           by (auto dest: hyp_member_super)
  1037         then show ?thesis
  1038         proof 
  1039           assume "G \<turnstile>Method super_new member_of C"
  1040           with super_new_override
  1041           show ?thesis
  1042             by blast
  1043         next
  1044           assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
  1045                   G \<turnstile>Method new member_of C"
  1046           with super_new_override show ?thesis
  1047             by (blast intro: stat_overridesR.Indirect) 
  1048         qed
  1049       qed
  1050     qed
  1051   qed
  1052 qed
  1053 
  1054 lemma non_Package_instance_method_inheritance_cases [consumes 6,
  1055          case_names Inheritance Overriding]:
  1056   assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
  1057               accmodi_old: "accmodi old \<noteq> Package" and 
  1058           instance_method: "\<not> is_static old" and
  1059                    subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
  1060              old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
  1061                        wf: "wf_prog G" and
  1062               inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
  1063                overriding: "\<And> new.
  1064                            \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
  1065                            \<Longrightarrow> P"
  1066   shows P
  1067 proof -
  1068   from old_inheritable accmodi_old instance_method subcls old_declared wf 
  1069        inheritance overriding
  1070   show ?thesis
  1071     by (auto dest: non_Package_instance_method_inheritance)
  1072 qed
  1073 
  1074 lemma dynamic_to_static_overriding:
  1075   assumes dyn_override: "G\<turnstile> new overrides old" and
  1076            accmodi_old: "accmodi old \<noteq> Package" and
  1077                     wf: "wf_prog G"
  1078   shows "G\<turnstile> new overrides\<^sub>S old"  
  1079 proof - 
  1080   from dyn_override accmodi_old
  1081   show ?thesis (is "?Overrides new old")
  1082   proof (induct rule: overridesR.induct)
  1083     case (Direct new old)
  1084     assume   new_declared: "G\<turnstile>Method new declared_in declclass new"
  1085     assume eq_sig_new_old: "msig new = msig old"
  1086     assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
  1087     assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and
  1088            "accmodi old \<noteq> Package" and
  1089            "\<not> is_static old" and
  1090            "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and
  1091            "G\<turnstile>Method old declared_in declclass old" 
  1092     from this wf
  1093     show "?Overrides new old"
  1094     proof (cases rule: non_Package_instance_method_inheritance_cases)
  1095       case Inheritance
  1096       assume "G \<turnstile>Method old member_of declclass new"
  1097       then have "G\<turnstile>mid (msig old) undeclared_in declclass new"
  1098       proof cases
  1099         case Immediate 
  1100         with subcls_new_old wf show ?thesis     
  1101           by (auto dest: subcls_irrefl)
  1102       next
  1103         case Inherited
  1104         then show ?thesis
  1105           by (cases old) auto
  1106       qed
  1107       with eq_sig_new_old new_declared
  1108       show ?thesis
  1109         by (cases old,cases new) (auto dest!: declared_not_undeclared)
  1110     next
  1111       case (Overriding new') 
  1112       assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old"
  1113       then have "msig new' = msig old"
  1114         by (auto dest: stat_overrides_commonD)
  1115       with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
  1116         by simp
  1117       assume "G \<turnstile>Method new' member_of declclass new"
  1118       then show ?thesis
  1119       proof (cases)
  1120         case Immediate
  1121         then have declC_new: "declclass new' = declclass new" 
  1122           by auto
  1123         from Immediate 
  1124         have "G\<turnstile>Method new' declared_in declclass new"
  1125           by (cases new') auto
  1126         with new_declared eq_sig_new_new' declC_new 
  1127         have "new=new'"
  1128           by (cases new, cases new') (auto dest: unique_declared_in) 
  1129         with stat_override_new'
  1130         show ?thesis
  1131           by simp
  1132       next
  1133         case Inherited
  1134         then have "G\<turnstile>mid (msig new') undeclared_in declclass new"
  1135           by (cases new') (auto)
  1136         with eq_sig_new_new' new_declared
  1137         show ?thesis
  1138           by (cases new,cases new') (auto dest!: declared_not_undeclared)
  1139       qed
  1140     qed
  1141   next
  1142     case (Indirect new inter old)
  1143     assume accmodi_old: "accmodi old \<noteq> Package"
  1144     assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old"
  1145     with accmodi_old 
  1146     have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old"
  1147       by blast
  1148     moreover 
  1149     assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter"
  1150     moreover
  1151     have "accmodi inter \<noteq> Package"
  1152     proof -
  1153       from stat_override_inter_old wf 
  1154       have "accmodi old \<le> accmodi inter"
  1155         by (auto dest: wf_prog_stat_overridesD)
  1156       with stat_override_inter_old accmodi_old
  1157       show ?thesis
  1158         by (auto dest!: no_Private_stat_override
  1159                  split: acc_modi.splits 
  1160                  dest: acc_modi_le_Dests)
  1161     qed
  1162     ultimately show "?Overrides new old"
  1163       by (blast intro: stat_overridesR.Indirect)
  1164   qed
  1165 qed
  1166 
  1167 lemma wf_prog_dyn_override_prop:
  1168   assumes dyn_override: "G \<turnstile> new overrides old" and
  1169                     wf: "wf_prog G"
  1170   shows "accmodi old \<le> accmodi new"
  1171 proof (cases "accmodi old = Package")
  1172   case True
  1173   note old_Package = this
  1174   show ?thesis
  1175   proof (cases "accmodi old \<le> accmodi new")
  1176     case True then show ?thesis .
  1177   next
  1178     case False
  1179     with old_Package 
  1180     have "accmodi new = Private"
  1181       by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
  1182     with dyn_override 
  1183     show ?thesis
  1184       by (auto dest: overrides_commonD)
  1185   qed    
  1186 next
  1187   case False
  1188   with dyn_override wf
  1189   have "G \<turnstile> new overrides\<^sub>S old"
  1190     by (blast intro: dynamic_to_static_overriding)
  1191   with wf 
  1192   show ?thesis
  1193    by (blast dest: wf_prog_stat_overridesD)
  1194 qed 
  1195 
  1196 lemma overrides_Package_old: 
  1197   assumes dyn_override: "G \<turnstile> new overrides old" and 
  1198            accmodi_new: "accmodi new = Package" and
  1199                     wf: "wf_prog G "
  1200   shows "accmodi old = Package"
  1201 proof (cases "accmodi old")
  1202   case Private
  1203   with dyn_override show ?thesis
  1204     by (simp add: no_Private_override)
  1205 next
  1206   case Package
  1207   then show ?thesis .
  1208 next
  1209   case Protected
  1210   with dyn_override wf
  1211   have "G \<turnstile> new overrides\<^sub>S old"
  1212     by (auto intro: dynamic_to_static_overriding)
  1213   with wf 
  1214   have "accmodi old \<le> accmodi new"
  1215     by (auto dest: wf_prog_stat_overridesD)
  1216   with Protected accmodi_new
  1217   show ?thesis
  1218     by (simp add: less_acc_def le_acc_def)
  1219 next
  1220   case Public
  1221   with dyn_override wf
  1222   have "G \<turnstile> new overrides\<^sub>S old"
  1223     by (auto intro: dynamic_to_static_overriding)
  1224   with wf 
  1225   have "accmodi old \<le> accmodi new"
  1226     by (auto dest: wf_prog_stat_overridesD)
  1227   with Public accmodi_new
  1228   show ?thesis
  1229     by (simp add: less_acc_def le_acc_def)
  1230 qed
  1231 
  1232 lemma dyn_override_Package:
  1233   assumes dyn_override: "G \<turnstile> new overrides old" and
  1234            accmodi_old: "accmodi old = Package" and 
  1235            accmodi_new: "accmodi new = Package" and
  1236                     wf: "wf_prog G"
  1237   shows "pid (declclass old) = pid (declclass new)"
  1238 proof - 
  1239   from dyn_override accmodi_old accmodi_new
  1240   show ?thesis (is "?EqPid old new")
  1241   proof (induct rule: overridesR.induct)
  1242     case (Direct new old)
  1243     assume "accmodi old = Package"
  1244            "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1245     then show "pid (declclass old) =  pid (declclass new)"
  1246       by (auto simp add: inheritable_in_def)
  1247   next
  1248     case (Indirect new inter old)
  1249     assume accmodi_old: "accmodi old = Package" and
  1250            accmodi_new: "accmodi new = Package" 
  1251     assume "G \<turnstile> new overrides inter"
  1252     with accmodi_new wf
  1253     have "accmodi inter = Package"
  1254       by  (auto intro: overrides_Package_old)
  1255     with Indirect
  1256     show "pid (declclass old) =  pid (declclass new)"
  1257       by auto
  1258   qed
  1259 qed
  1260 
  1261 lemma dyn_override_Package_escape:
  1262   assumes dyn_override: "G \<turnstile> new overrides old" and
  1263            accmodi_old: "accmodi old = Package" and 
  1264           outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
  1265                     wf: "wf_prog G"
  1266   shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
  1267              pid (declclass old) = pid (declclass inter) \<and>
  1268              Protected \<le> accmodi inter"
  1269 proof -
  1270   from dyn_override accmodi_old outside_pack
  1271   show ?thesis (is "?P new old")
  1272   proof (induct rule: overridesR.induct)
  1273     case (Direct new old)
  1274     assume accmodi_old: "accmodi old = Package"
  1275     assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1276     assume "G \<turnstile>Method old inheritable_in pid (declclass new)"
  1277     with accmodi_old 
  1278     have "pid (declclass old) = pid (declclass new)"
  1279       by (simp add: inheritable_in_def)
  1280     with outside_pack 
  1281     show "?P new old"
  1282       by (contradiction)
  1283   next
  1284     case (Indirect new inter old)
  1285     assume accmodi_old: "accmodi old = Package"
  1286     assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
  1287     assume override_new_inter: "G \<turnstile> new overrides inter"
  1288     assume override_inter_old: "G \<turnstile> inter overrides old"
  1289     assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 
  1290                            pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk>
  1291                            \<Longrightarrow> ?P new inter"
  1292     assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 
  1293                            pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk>
  1294                            \<Longrightarrow> ?P inter old"
  1295     show "?P new old"
  1296     proof (cases "pid (declclass old) = pid (declclass inter)")
  1297       case True
  1298       note same_pack_old_inter = this
  1299       show ?thesis
  1300       proof (cases "pid (declclass inter) = pid (declclass new)")
  1301         case True
  1302         with same_pack_old_inter outside_pack
  1303         show ?thesis
  1304           by auto
  1305       next
  1306         case False
  1307         note diff_pack_inter_new = this
  1308         show ?thesis
  1309         proof (cases "accmodi inter = Package")
  1310           case True
  1311           with diff_pack_inter_new hyp_new_inter  
  1312           obtain newinter where
  1313             over_new_newinter: "G \<turnstile> new overrides newinter" and
  1314             over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
  1315             eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
  1316             accmodi_newinter: "Protected \<le> accmodi newinter"
  1317             by auto
  1318           from over_newinter_inter override_inter_old
  1319           have "G\<turnstile>newinter overrides old"
  1320             by (rule overridesR.Indirect)
  1321           moreover
  1322           from eq_pid same_pack_old_inter 
  1323           have "pid (declclass old) = pid (declclass newinter)"
  1324             by simp
  1325           moreover
  1326           note over_new_newinter accmodi_newinter
  1327           ultimately show ?thesis
  1328             by blast
  1329         next
  1330           case False
  1331           with override_new_inter
  1332           have "Protected \<le> accmodi inter"
  1333             by (cases "accmodi inter") (auto dest: no_Private_override)
  1334           with override_new_inter override_inter_old same_pack_old_inter
  1335           show ?thesis
  1336             by blast
  1337         qed
  1338       qed
  1339     next
  1340       case False
  1341       with accmodi_old hyp_inter_old
  1342       obtain newinter where
  1343         over_inter_newinter: "G \<turnstile> inter overrides newinter" and
  1344           over_newinter_old: "G \<turnstile> newinter overrides old" and 
  1345                 eq_pid: "pid (declclass old) = pid (declclass newinter)" and
  1346         accmodi_newinter: "Protected \<le> accmodi newinter"
  1347         by auto
  1348       from override_new_inter over_inter_newinter 
  1349       have "G \<turnstile> new overrides newinter"
  1350         by (rule overridesR.Indirect)
  1351       with eq_pid over_newinter_old accmodi_newinter
  1352       show ?thesis
  1353         by blast
  1354     qed
  1355   qed
  1356 qed
  1357 
  1358 lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
  1359 
  1360 lemma declclass_widen[rule_format]: 
  1361  "wf_prog G 
  1362  \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  1363  \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
  1364 proof (induct G C rule: class_rec_induct', intro allI impI)
  1365   fix G C c m
  1366   assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object
  1367                \<Longrightarrow> ?P G (super c)"
  1368   assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  1369          m:  "methd G C sig = Some m"
  1370   show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
  1371   proof (cases "C=Object")
  1372     case True 
  1373     with wf m show ?thesis by (simp add: methd_Object_SomeD)
  1374   next
  1375     let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  1376     let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1377     case False 
  1378     with cls_C wf m
  1379     have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  1380       by (simp add: methd_rec)
  1381     show ?thesis
  1382     proof (cases "?table sig")
  1383       case None
  1384       from this methd_C have "?filter (methd G (super c)) sig = Some m"
  1385         by simp
  1386       moreover
  1387       from wf cls_C False obtain sup where "class G (super c) = Some sup"
  1388         by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1389       moreover note wf False cls_C  
  1390       ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  
  1391         by (auto intro: Hyp [rule_format])
  1392       moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C1 super c" by (rule subcls1I)
  1393       ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
  1394     next
  1395       case Some
  1396       from this wf False cls_C methd_C show ?thesis by auto
  1397     qed
  1398   qed
  1399 qed
  1400 
  1401 lemma declclass_methd_Object: 
  1402  "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object"
  1403 by auto
  1404 
  1405 lemma methd_declaredD: 
  1406  "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 
  1407   \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1408 proof -
  1409   assume    wf: "wf_prog G"
  1410   then have ws: "ws_prog G" ..
  1411   assume  clsC: "is_class G C"
  1412   from clsC ws 
  1413   show "methd G C sig = Some m 
  1414         \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
  1415   proof (induct C rule: ws_class_induct')
  1416     case Object
  1417     assume "methd G Object sig = Some m" 
  1418     with wf show ?thesis
  1419       by - (rule method_declared_inI, auto) 
  1420   next
  1421     case Subcls
  1422     fix C c
  1423     assume clsC: "class G C = Some c"
  1424     and       m: "methd G C sig = Some m"
  1425     and     hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 
  1426     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1427     show ?thesis
  1428     proof (cases "?newMethods sig")
  1429       case None
  1430       from None ws clsC m hyp 
  1431       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
  1432     next
  1433       case Some
  1434       from Some ws clsC m 
  1435       show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
  1436     qed
  1437   qed
  1438 qed
  1439 
  1440 lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
  1441   assumes methd_C: "methd G C sig = Some m" and
  1442                ws: "ws_prog G" and
  1443              clsC: "class G C = Some c" and
  1444         neq_C_Obj: "C\<noteq>Object"
  1445   shows
  1446 "\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
  1447   \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
  1448  \<rbrakk> \<Longrightarrow> P"
  1449 proof -
  1450   let ?inherited   = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 
  1451                               (methd G (super c))"
  1452   let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  1453   from ws clsC neq_C_Obj methd_C 
  1454   have methd_unfold: "(?inherited ++ ?new) sig = Some m"
  1455     by (simp add: methd_rec)
  1456   assume NewMethod: "?new sig = Some m \<Longrightarrow> P"
  1457   assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); 
  1458                             methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P"
  1459   show P
  1460   proof (cases "?new sig")
  1461     case None
  1462     with methd_unfold have "?inherited sig = Some m"
  1463       by (auto)
  1464     with InheritedMethod show P by blast
  1465   next
  1466     case Some
  1467     with methd_unfold have "?new sig = Some m"
  1468       by auto
  1469     with NewMethod show P by blast
  1470   qed
  1471 qed
  1472 
  1473   
  1474 lemma methd_member_of:
  1475   assumes wf: "wf_prog G"
  1476   shows
  1477     "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
  1478   (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
  1479 proof -
  1480   from wf   have   ws: "ws_prog G" ..
  1481   assume defC: "is_class G C"
  1482   from defC ws 
  1483   show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
  1484   proof (induct rule: ws_class_induct')  
  1485     case Object
  1486     with wf have declC: "Object = declclass m"
  1487       by (simp add: declclass_methd_Object)
  1488     from Object wf have "G\<turnstile>Methd sig m declared_in Object"
  1489       by (auto intro: methd_declaredD simp add: declC)
  1490     with declC 
  1491     show "?MemberOf Object"
  1492       by (auto intro!: members.Immediate
  1493                   simp del: methd_Object)
  1494   next
  1495     case (Subcls C c)
  1496     assume  clsC: "class G C = Some c" and
  1497        neq_C_Obj: "C \<noteq> Object"  
  1498     assume methd: "?Method C"
  1499     from methd ws clsC neq_C_Obj
  1500     show "?MemberOf C"
  1501     proof (cases rule: methd_rec_Some_cases)
  1502       case NewMethod
  1503       with clsC show ?thesis
  1504         by (auto dest: method_declared_inI intro!: members.Immediate)
  1505     next
  1506       case InheritedMethod
  1507       then show "?thesis"
  1508         by (blast dest: inherits_member)
  1509     qed
  1510   qed
  1511 qed
  1512 
  1513 lemma current_methd: 
  1514       "\<lbrakk>table_of (methods c) sig = Some new;
  1515         ws_prog G; class G C = Some c; C \<noteq> Object; 
  1516         methd G (super c) sig = Some old\<rbrakk> 
  1517     \<Longrightarrow> methd G C sig = Some (C,new)"
  1518 by (auto simp add: methd_rec
  1519             intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)
  1520 
  1521 lemma wf_prog_staticD:
  1522   assumes     wf: "wf_prog G" and
  1523             clsC: "class G C = Some c" and
  1524        neq_C_Obj: "C \<noteq> Object" and 
  1525              old: "methd G (super c) sig = Some old" and 
  1526      accmodi_old: "Protected \<le> accmodi old" and
  1527              new: "table_of (methods c) sig = Some new"
  1528   shows "is_static new = is_static old"
  1529 proof -
  1530   from clsC wf 
  1531   have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
  1532   from wf clsC neq_C_Obj
  1533   have is_cls_super: "is_class G (super c)" 
  1534     by (blast dest: wf_prog_acc_superD is_acc_classD)
  1535   from wf is_cls_super old 
  1536   have old_member_of: "G\<turnstile>Methd sig old member_of (super c)"  
  1537     by (rule methd_member_of)
  1538   from old wf is_cls_super 
  1539   have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)"
  1540     by (auto dest: methd_declared_in_declclass)
  1541   from new clsC 
  1542   have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C"
  1543     by (auto intro: method_declared_inI)
  1544   note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
  1545   from clsC neq_C_Obj
  1546   have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c"
  1547     by (rule subcls1I)
  1548   then have "G\<turnstile>C \<prec>\<^sub>C super c" ..
  1549   also from old wf is_cls_super
  1550   have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC)
  1551   finally have subcls_C_old:  "G\<turnstile>C \<prec>\<^sub>C (declclass old)" .
  1552   from accmodi_old 
  1553   have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C"
  1554     by (auto simp add: inheritable_in_def
  1555                  dest: acc_modi_le_Dests)
  1556   show ?thesis
  1557   proof (cases "is_static new")
  1558     case True
  1559     with subcls_C_old new_declared old_declared inheritable
  1560     have "G,sig\<turnstile>(C,new) hides old"
  1561       by (auto intro: hidesI)
  1562     with True wf_cdecl neq_C_Obj new 
  1563     show ?thesis
  1564       by (auto dest: wf_cdecl_hides_SomeD)
  1565   next
  1566     case False
  1567     with subcls_C_old new_declared old_declared inheritable subcls1_C_super
  1568          old_member_of
  1569     have "G,sig\<turnstile>(C,new) overrides\<^sub>S old"
  1570       by (auto intro: stat_overridesR.Direct)
  1571     with False wf_cdecl neq_C_Obj new 
  1572     show ?thesis
  1573       by (auto dest: wf_cdecl_overrides_SomeD)
  1574   qed
  1575 qed
  1576 
  1577 lemma inheritable_instance_methd: 
  1578   assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1579               is_cls_D: "is_class G D" and
  1580                     wf: "wf_prog G" and 
  1581                    old: "methd G D sig = Some old" and
  1582            accmodi_old: "Protected \<le> accmodi old" and  
  1583         not_static_old: "\<not> is_static old"
  1584   shows
  1585   "\<exists>new. methd G C sig = Some new \<and>
  1586          (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
  1587  (is "(\<exists>new. (?Constraint C new old))")
  1588 proof -
  1589   from subclseq_C_D is_cls_D 
  1590   have is_cls_C: "is_class G C" by (rule subcls_is_class2) 
  1591   from wf 
  1592   have ws: "ws_prog G" ..
  1593   from is_cls_C ws subclseq_C_D 
  1594   show "\<exists>new. ?Constraint C new old"
  1595   proof (induct rule: ws_class_induct')
  1596     case (Object co)
  1597     then have eq_D_Obj: "D=Object" by auto
  1598     with old 
  1599     have "?Constraint Object old old"
  1600       by auto
  1601     with eq_D_Obj 
  1602     show "\<exists> new. ?Constraint Object new old" by auto
  1603   next
  1604     case (Subcls C c)
  1605     assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old"
  1606     assume clsC: "class G C = Some c"
  1607     assume neq_C_Obj: "C\<noteq>Object"
  1608     from clsC wf 
  1609     have wf_cdecl: "wf_cdecl G (C,c)" 
  1610       by (rule wf_prog_cdecl)
  1611     from ws clsC neq_C_Obj
  1612     have is_cls_super: "is_class G (super c)"
  1613       by (auto dest: ws_prog_cdeclD)
  1614     from clsC wf neq_C_Obj 
  1615     have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and
  1616          subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c"
  1617       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
  1618               intro: subcls1I)
  1619     show "\<exists>new. ?Constraint C new old"
  1620     proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D")
  1621       case False
  1622       from False Subcls 
  1623       have eq_C_D: "C=D"
  1624         by (auto dest: subclseq_superD)
  1625       with old 
  1626       have "?Constraint C old old"
  1627         by auto
  1628       with eq_C_D 
  1629       show "\<exists> new. ?Constraint C new old" by auto
  1630     next
  1631       case True
  1632       with hyp obtain super_method
  1633         where super: "?Constraint (super c) super_method old" by blast
  1634       from super not_static_old
  1635       have not_static_super: "\<not> is_static super_method"
  1636         by (auto dest!: stat_overrides_commonD)
  1637       from super old wf accmodi_old
  1638       have accmodi_super_method: "Protected \<le> accmodi super_method"
  1639         by (auto dest!: wf_prog_stat_overridesD)
  1640       from super accmodi_old wf
  1641       have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
  1642         by (auto dest!: wf_prog_stat_overridesD
  1643                         acc_modi_le_Dests
  1644               simp add: inheritable_in_def)                
  1645       from super wf is_cls_super
  1646       have member: "G\<turnstile>Methd sig super_method member_of (super c)"
  1647         by (auto intro: methd_member_of) 
  1648       from member
  1649       have decl_super_method:
  1650         "G\<turnstile>Methd sig super_method declared_in (declclass super_method)"
  1651         by (auto dest: member_of_declC)
  1652       from super subcls1_C_super ws is_cls_super 
  1653       have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)"
  1654         by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 
  1655       show "\<exists> new. ?Constraint C new old"
  1656       proof (cases "methd G C sig")
  1657         case None
  1658         have "methd G (super c) sig = None"
  1659         proof -
  1660           from clsC ws None 
  1661           have no_new: "table_of (methods c) sig = None" 
  1662             by (auto simp add: methd_rec)
  1663           with clsC 
  1664           have undeclared: "G\<turnstile>mid sig undeclared_in C"
  1665             by (auto simp add: undeclared_in_def cdeclaredmethd_def)
  1666           with inheritable member superAccessible subcls1_C_super
  1667           have inherits: "G\<turnstile>C inherits (method sig super_method)"
  1668             by (auto simp add: inherits_def)
  1669           with clsC ws no_new super neq_C_Obj
  1670           have "methd G C sig = Some super_method"
  1671             by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
  1672           with None show ?thesis
  1673             by simp
  1674         qed
  1675         with super show ?thesis by auto
  1676       next
  1677         case (Some new)
  1678         from this ws clsC neq_C_Obj
  1679         show ?thesis
  1680         proof (cases rule: methd_rec_Some_cases)
  1681           case InheritedMethod
  1682           with super Some show ?thesis 
  1683             by auto
  1684         next
  1685           case NewMethod
  1686           assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig 
  1687                        = Some new"
  1688           from new 
  1689           have declcls_new: "declclass new = C" 
  1690             by auto
  1691           from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
  1692           have not_static_new: "\<not> is_static new" 
  1693             by (auto dest: wf_prog_staticD) 
  1694           from clsC new
  1695           have decl_new: "G\<turnstile>Methd sig new declared_in C"
  1696             by (auto simp add: declared_in_def cdeclaredmethd_def)
  1697           from not_static_new decl_new decl_super_method
  1698                member subcls1_C_super inheritable declcls_new subcls_C_super 
  1699           have "G,sig\<turnstile> new overrides\<^sub>S super_method"
  1700             by (auto intro: stat_overridesR.Direct) 
  1701           with super Some
  1702           show ?thesis
  1703             by (auto intro: stat_overridesR.Indirect)
  1704         qed
  1705       qed
  1706     qed
  1707   qed
  1708 qed
  1709 
  1710 lemma inheritable_instance_methd_cases [consumes 6
  1711                                        , case_names Inheritance Overriding]: 
  1712   assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1713               is_cls_D: "is_class G D" and
  1714                     wf: "wf_prog G" and 
  1715                    old: "methd G D sig = Some old" and
  1716            accmodi_old: "Protected \<le> accmodi old" and  
  1717         not_static_old: "\<not> is_static old" and
  1718            inheritance:  "methd G C sig = Some old \<Longrightarrow> P" and
  1719             overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
  1720                                    G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
  1721         
  1722   shows P
  1723 proof -
  1724 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1725 show ?thesis
  1726   by (auto dest: inheritable_instance_methd intro: inheritance overriding)
  1727 qed
  1728 
  1729 lemma inheritable_instance_methd_props: 
  1730   assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
  1731               is_cls_D: "is_class G D" and
  1732                     wf: "wf_prog G" and 
  1733                    old: "methd G D sig = Some old" and
  1734            accmodi_old: "Protected \<le> accmodi old" and  
  1735         not_static_old: "\<not> is_static old"
  1736   shows
  1737   "\<exists>new. methd G C sig = Some new \<and>
  1738           \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
  1739  (is "(\<exists>new. (?Constraint C new old))")
  1740 proof -
  1741   from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  1742   show ?thesis
  1743   proof (cases rule: inheritable_instance_methd_cases)
  1744     case Inheritance
  1745     with not_static_old accmodi_old show ?thesis by auto
  1746   next
  1747     case (Overriding new)
  1748     then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
  1749     with Overriding not_static_old accmodi_old wf 
  1750     show ?thesis 
  1751       by (auto dest!: wf_prog_stat_overridesD)
  1752   qed
  1753 qed
  1754               
  1755 (* local lemma *)
  1756 lemma bexI': "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x" by blast
  1757 lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast
  1758 
  1759 lemma subint_widen_imethds: 
  1760   assumes irel: "G\<turnstile>I\<preceq>I J"
  1761   and wf: "wf_prog G"
  1762   and is_iface: "is_iface G J"
  1763   and jm: "jm \<in> imethds G J sig"
  1764   shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and> 
  1765                           accmodi im = accmodi jm \<and>
  1766                           G\<turnstile>resTy im\<preceq>resTy jm"
  1767   using irel jm
  1768 proof (induct rule: converse_rtrancl_induct)
  1769     case base
  1770     then show ?case by  (blast elim: bexI')
  1771   next
  1772     case (step I SI)
  1773     from `G\<turnstile>I \<prec>I1 SI`
  1774     obtain i where
  1775       ifI: "iface G I = Some i" and
  1776        SI: "SI \<in> set (isuperIfs i)"
  1777       by (blast dest: subint1D)
  1778 
  1779     let ?newMethods 
  1780           = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
  1781     show ?case
  1782     proof (cases "?newMethods sig = {}")
  1783       case True
  1784       with ifI SI step wf
  1785       show "?thesis" 
  1786         by (auto simp add: imethds_rec) 
  1787     next
  1788       case False
  1789       from ifI wf False
  1790       have imethds: "imethds G I sig = ?newMethods sig"
  1791         by (simp add: imethds_rec)
  1792       from False
  1793       obtain im where
  1794         imdef: "im \<in> ?newMethods sig" 
  1795         by (blast)
  1796       with imethds 
  1797       have im: "im \<in> imethds G I sig"
  1798         by (blast)
  1799       with im wf ifI 
  1800       obtain
  1801          imStatic: "\<not> is_static im" and
  1802          imPublic: "accmodi im = Public"
  1803         by (auto dest!: imethds_wf_mhead)       
  1804       from ifI wf 
  1805       have wf_I: "wf_idecl G (I,i)" 
  1806         by (rule wf_prog_idecl)
  1807       with SI wf  
  1808       obtain si where
  1809          ifSI: "iface G SI = Some si" and
  1810         wf_SI: "wf_idecl G (SI,si)" 
  1811         by (auto dest!: wf_idecl_supD is_acc_ifaceD
  1812                   dest: wf_prog_idecl)
  1813       from step
  1814       obtain sim::"qtname \<times> mhead"  where
  1815                       sim: "sim \<in> imethds G SI sig" and
  1816          eq_static_sim_jm: "is_static sim = is_static jm" and 
  1817          eq_access_sim_jm: "accmodi sim = accmodi jm" and 
  1818         resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm"
  1819         by blast
  1820       with wf_I SI imdef sim 
  1821       have "G\<turnstile>resTy im\<preceq>resTy sim"   
  1822         by (auto dest!: wf_idecl_hidings hidings_entailsD)
  1823       with wf resTy_widen_sim_jm 
  1824       have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm"
  1825         by (blast intro: widen_trans)
  1826       from sim wf ifSI  
  1827       obtain
  1828         simStatic: "\<not> is_static sim" and
  1829         simPublic: "accmodi sim = Public"
  1830         by (auto dest!: imethds_wf_mhead)
  1831       from im 
  1832            imStatic simStatic eq_static_sim_jm
  1833            imPublic simPublic eq_access_sim_jm
  1834            resTy_widen_im_jm
  1835       show ?thesis 
  1836         by auto 
  1837     qed
  1838 qed
  1839      
  1840 (* Tactical version *)
  1841 (* 
  1842 lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow>  
  1843   \<forall> jm \<in> imethds G J sig.  
  1844   \<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> 
  1845                           access (mthd im)= access (mthd jm) \<and>
  1846                           G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)"
  1847 apply (erule converse_rtrancl_induct)
  1848 apply  (clarsimp elim!: bexI')
  1849 apply (frule subint1D)
  1850 apply clarify
  1851 apply (erule ballE')
  1852 apply  fast
  1853 apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl)
  1854 apply clarsimp
  1855 apply (subst imethds_rec, assumption, erule wf_ws_prog)
  1856 apply (unfold overrides_t_def)
  1857 apply (drule (1) wf_prog_idecl)
  1858 apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
  1859                                        [THEN is_acc_ifaceD [THEN conjunct1]]]])
  1860 apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
  1861                   sig ={}")
  1862 apply   force
  1863 
  1864 apply   (simp only:)
  1865 apply   (simp)
  1866 apply   clarify
  1867 apply   (frule wf_idecl_hidings [THEN hidings_entailsD])
  1868 apply     blast
  1869 apply     blast
  1870 apply   (rule bexI')
  1871 apply     simp
  1872 apply     (drule table_of_map_SomeI [of _ "sig"])
  1873 apply     simp
  1874 
  1875 apply     (frule wf_idecl_mhead [of _ _ _ "sig"])
  1876 apply       (rule table_of_Some_in_set)
  1877 apply       assumption
  1878 apply     auto
  1879 done
  1880 *)
  1881     
  1882 
  1883 (* local lemma *)
  1884 lemma implmt1_methd: 
  1885  "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow>  
  1886   \<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> 
  1887                        G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1888                        accmodi im = Public \<and> accmodi cm = Public"
  1889 apply (drule implmt1D)
  1890 apply clarify
  1891 apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
  1892 apply (frule (1) imethds_wf_mhead)
  1893 apply  (simp add: is_acc_iface_def)
  1894 apply (force)
  1895 done
  1896 
  1897 
  1898 (* local lemma *)
  1899 lemma implmt_methd [rule_format (no_asm)]: 
  1900 "\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow>  
  1901  (\<forall> im    \<in>imethds G I   sig.  
  1902   \<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> 
  1903                       G\<turnstile>resTy cm\<preceq>resTy im \<and>
  1904                       accmodi im = Public \<and> accmodi cm = Public)"
  1905 apply (frule implmt_is_class)
  1906 apply (erule implmt.induct)
  1907 apply   safe
  1908 apply   (drule (2) implmt1_methd)
  1909 apply   fast
  1910 apply  (drule (1) subint_widen_imethds)
  1911 apply   simp
  1912 apply   assumption
  1913 apply  clarify
  1914 apply  (drule (2) implmt1_methd)
  1915 apply  (force)
  1916 apply (frule subcls1D)
  1917 apply (drule (1) bspec)
  1918 apply clarify
  1919 apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 
  1920                                  OF _ implmt_is_class])
  1921 apply auto 
  1922 done
  1923 
  1924 lemma mheadsD [rule_format (no_asm)]: 
  1925 "emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow>
  1926  (\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> 
  1927           accmethd G S C sig = Some m \<and>
  1928           (declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or>
  1929  (\<exists>I. t = IfaceT I \<and> ((\<exists>im. im  \<in> accimethds G (pid S) I sig \<and> 
  1930           mthd im = mhd emh) \<or> 
  1931   (\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> 
  1932        accmodi m \<noteq> Private \<and> 
  1933        declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or>
  1934  (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and>
  1935         accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 
  1936         declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)"
  1937 apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1])
  1938 apply auto
  1939 apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
  1940 apply (auto  dest!: accmethd_SomeD)
  1941 done
  1942 
  1943 lemma mheads_cases [consumes 2, case_names Class_methd 
  1944                     Iface_methd Iface_Object_methd Array_Object_methd]: 
  1945 "\<lbrakk>emh \<in> mheads G S t sig; wf_prog G;
  1946  \<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m;
  1947            (declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh; 
  1948  \<And> I im. \<lbrakk>t = IfaceT I; im  \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk>
  1949           \<Longrightarrow> P emh;
  1950  \<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S);
  1951           accmethd G S Object sig = Some m; accmodi m \<noteq> Private;
  1952          declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh;
  1953  \<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S);
  1954           accmethd G S Object sig = Some m; accmodi m \<noteq> Private; 
  1955           declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow>  P emh 
  1956 \<rbrakk> \<Longrightarrow> P emh"
  1957 by (blast dest!: mheadsD)
  1958 
  1959 lemma declclassD[rule_format]:
  1960  "\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; 
  1961    class G (declclass m) = Some d\<rbrakk>
  1962   \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)"
  1963 proof -
  1964   assume    wf: "wf_prog G"
  1965   then have ws: "ws_prog G" ..
  1966   assume  clsC: "class G C = Some c"
  1967   from clsC ws 
  1968   show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk>
  1969         \<Longrightarrow> table_of (methods d) sig  = Some (mthd m)" 
  1970   proof (induct rule: ws_class_induct)
  1971     case Object
  1972     with wf show "?thesis m d" by auto
  1973   next
  1974     case (Subcls C c)
  1975     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
  1976     show "?thesis m d" 
  1977     proof (cases "?newMethods")
  1978       case None
  1979       from None ws Subcls
  1980       show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
  1981     next
  1982       case Some
  1983       from Some ws Subcls
  1984       show "?thesis" 
  1985         by (auto simp add: methd_rec
  1986                      dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  1987     qed
  1988   qed
  1989 qed
  1990 
  1991 lemma dynmethd_Object:
  1992   assumes statM: "methd G Object sig = Some statM" and
  1993         private: "accmodi statM = Private" and 
  1994        is_cls_C: "is_class G C" and
  1995              wf: "wf_prog G"
  1996   shows "dynmethd G Object C sig = Some statM"
  1997 proof -
  1998   from is_cls_C wf 
  1999   have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
  2000     by (auto intro: subcls_ObjectI)
  2001   from wf have ws: "ws_prog G" 
  2002     by simp
  2003   from wf 
  2004   have is_cls_Obj: "is_class G Object" 
  2005     by simp
  2006   from statM subclseq is_cls_Obj ws private
  2007   show ?thesis
  2008   proof (cases rule: dynmethd_cases)
  2009     case Static then show ?thesis .
  2010   next
  2011     case Overrides 
  2012     with private show ?thesis 
  2013       by (auto dest: no_Private_override)
  2014   qed
  2015 qed
  2016 
  2017 lemma wf_imethds_hiding_objmethdsD: 
  2018   assumes     old: "methd G Object sig = Some old" and
  2019           is_if_I: "is_iface G I" and
  2020                wf: "wf_prog G" and    
  2021       not_private: "accmodi old \<noteq> Private" and
  2022               new: "new \<in> imethds G I sig" 
  2023   shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
  2024 proof -
  2025   from wf have ws: "ws_prog G" by simp
  2026   {
  2027     fix I i new
  2028     assume ifI: "iface G I = Some i"
  2029     assume new: "table_of (imethods i) sig = Some new" 
  2030     from ifI new not_private wf old  
  2031     have "?P (I,new)"
  2032       by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
  2033             simp del: methd_Object)
  2034   } note hyp_newmethod = this  
  2035   from is_if_I ws new 
  2036   show ?thesis
  2037   proof (induct rule: ws_interface_induct)
  2038     case (Step I i)
  2039     assume ifI: "iface G I = Some i" 
  2040     assume new: "new \<in> imethds G I sig" 
  2041     from Step
  2042     have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)"
  2043       by auto 
  2044     from new ifI ws
  2045     show "?P new"
  2046     proof (cases rule: imethds_cases)
  2047       case NewMethod
  2048       with ifI hyp_newmethod
  2049       show ?thesis
  2050         by auto
  2051     next
  2052       case (InheritedMethod J)
  2053       assume "J \<in> set (isuperIfs i)" 
  2054              "new \<in> imethds G J sig"
  2055       with hyp 
  2056       show "?thesis"
  2057         by auto
  2058     qed
  2059   qed
  2060 qed
  2061 
  2062 text {*
  2063 Which dynamic classes are valid to look up a member of a distinct static type?
  2064 We have to distinct class members (named static members in Java) 
  2065 from instance members. Class members are global to all Objects of a class,
  2066 instance members are local to a single Object instance. If a member is
  2067 equipped with the static modifier it is a class member, else it is an 
  2068 instance member.
  2069 The following table gives an overview of the current framework. We assume
  2070 to have a reference with static type statT and a dynamic class dynC. Between
  2071 both of these types the widening relation holds 
  2072 @{term "G\<turnstile>Class dynC\<preceq> statT"}. Unfortunately this ordinary widening relation 
  2073 isn't enough to describe the valid lookup classes, since we must cope the
  2074 special cases of arrays and interfaces,too. If we statically expect an array or
  2075 inteface we may lookup a field or a method in Object which isn't covered in 
  2076 the widening relation.
  2077 
  2078 statT      field         instance method       static (class) method
  2079 ------------------------------------------------------------------------
  2080  NullT      /                  /                   /
  2081  Iface      /                dynC                Object
  2082  Class    dynC               dynC                 dynC
  2083  Array      /                Object              Object
  2084 
  2085 In most cases we con lookup the member in the dynamic class. But as an
  2086 interface can't declare new static methods, nor an array can define new
  2087 methods at all, we have to lookup methods in the base class Object.
  2088 
  2089 The limitation to classes in the field column is artificial  and comes out
  2090 of the typing rule for the field access (see rule @{text "FVar"} in the 
  2091 welltyping relation @{term "wt"} in theory WellType). 
  2092 I stems out of the fact, that Object
  2093 indeed has no non private fields. So interfaces and arrays can actually
  2094 have no fields at all and a field access would be senseless. (In Java
  2095 interfaces are allowed to declare new fields but in current Bali not!).
  2096 So there is no principal reason why we should not allow Objects to declare
  2097 non private fields. Then we would get the following column:
  2098        
  2099  statT    field
  2100 ----------------- 
  2101  NullT      /  
  2102  Iface    Object 
  2103  Class    dynC 
  2104  Array    Object
  2105 *}
  2106 primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
  2107                         ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
  2108 where
  2109   "G,NullT    \<turnstile> dynC valid_lookup_cls_for static_membr = False"
  2110 | "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 
  2111                 = (if static_membr 
  2112                       then dynC=Object 
  2113                       else G\<turnstile>Class dynC\<preceq> Iface I)"
  2114 | "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
  2115 | "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
  2116 
  2117 lemma valid_lookup_cls_is_class:
  2118   assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
  2119       ty_statT: "isrtype G statT" and
  2120             wf: "wf_prog G"
  2121   shows "is_class G dynC"
  2122 proof (cases statT)
  2123   case NullT
  2124   with dynC ty_statT show ?thesis
  2125     by (auto dest: widen_NT2)
  2126 next
  2127   case (IfaceT I)
  2128   with dynC wf show ?thesis
  2129     by (auto dest: implmt_is_class)
  2130 next
  2131   case (ClassT C)
  2132   with dynC ty_statT show ?thesis
  2133     by (auto dest: subcls_is_class2)
  2134 next
  2135   case (ArrayT T)
  2136   with dynC wf show ?thesis
  2137     by (auto)
  2138 qed
  2139 
  2140 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2141 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
  2142 declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
  2143 
  2144 lemma dynamic_mheadsD:   
  2145 "\<lbrakk>emh \<in> mheads G S statT sig;    
  2146   G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh);
  2147   isrtype G statT; wf_prog G
  2148  \<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: 
  2149           is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh"
  2150 proof - 
  2151   assume      emh: "emh \<in> mheads G S statT sig"
  2152   and          wf: "wf_prog G"
  2153   and   dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)"
  2154   and      istype: "isrtype G statT"
  2155   from dynC_Prop istype wf 
  2156   obtain y where
  2157     dynC: "class G dynC = Some y" 
  2158     by (auto dest: valid_lookup_cls_is_class)
  2159   from emh wf show ?thesis
  2160   proof (cases rule: mheads_cases)
  2161     case Class_methd
  2162     fix statC statDeclC sm
  2163     assume     statC: "statT = ClassT statC"
  2164     assume            "accmethd G S statC sig = Some sm"
  2165     then have     sm: "methd G statC sig = Some sm" 
  2166       by (blast dest: accmethd_SomeD)  
  2167     assume eq_mheads: "mhead (mthd sm) = mhd emh"
  2168     from statC 
  2169     have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
  2170       by (simp add: dynlookup_def)
  2171     from wf statC istype dynC_Prop sm 
  2172     obtain dm where
  2173       "dynmethd G statC dynC sig = Some dm"
  2174       "is_static dm = is_static sm" 
  2175       "G\<turnstile>resTy dm\<preceq>resTy sm"  
  2176       by (force dest!: ws_dynmethd accmethd_SomeD)
  2177     with dynlookup eq_mheads 
  2178     show ?thesis 
  2179       by (cases emh type: prod) (auto)
  2180   next
  2181     case Iface_methd
  2182     fix I im
  2183     assume    statI: "statT = IfaceT I" and
  2184           eq_mheads: "mthd im = mhd emh" and
  2185                      "im \<in> accimethds G (pid S) I sig" 
  2186     then have im: "im \<in> imethds G I sig" 
  2187       by (blast dest: accimethdsD)
  2188     with istype statI eq_mheads wf 
  2189     have not_static_emh: "\<not> is_static emh"
  2190       by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2191     from statI im
  2192     have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2193       by (auto simp add: dynlookup_def dynimethd_def) 
  2194     from wf dynC_Prop statI istype im not_static_emh 
  2195     obtain dm where
  2196       "methd G dynC sig = Some dm"
  2197       "is_static dm = is_static im" 
  2198       "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2199       by (force dest: implmt_methd)
  2200     with dynlookup eq_mheads
  2201     show ?thesis 
  2202       by (cases emh type: prod) (auto)
  2203   next
  2204     case Iface_Object_methd
  2205     fix I sm
  2206     assume   statI: "statT = IfaceT I" and
  2207                 sm: "accmethd G S Object sig = Some sm" and 
  2208          eq_mheads: "mhead (mthd sm) = mhd emh" and
  2209              nPriv: "accmodi sm \<noteq> Private"
  2210      show ?thesis 
  2211      proof (cases "imethds G I sig = {}")
  2212        case True
  2213        with statI 
  2214        have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig"
  2215          by (simp add: dynlookup_def dynimethd_def)
  2216        from wf dynC 
  2217        have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2218          by (auto intro: subcls_ObjectI)
  2219        from wf dynC dynC_Prop istype sm subclsObj 
  2220        obtain dm where
  2221          "dynmethd G Object dynC sig = Some dm"
  2222          "is_static dm = is_static sm" 
  2223          "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)"  
  2224          by (auto dest!: ws_dynmethd accmethd_SomeD 
  2225                   intro: class_Object [OF wf] intro: that)
  2226        with dynlookup eq_mheads
  2227        show ?thesis 
  2228          by (cases emh type: prod) (auto)
  2229      next
  2230        case False
  2231        with statI
  2232        have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
  2233          by (simp add: dynlookup_def dynimethd_def)
  2234        from istype statI
  2235        have "is_iface G I"
  2236          by auto
  2237        with wf sm nPriv False 
  2238        obtain im where
  2239               im: "im \<in> imethds G I sig" and
  2240          eq_stat: "is_static im = is_static sm" and
  2241          resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)"
  2242          by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD)
  2243        from im wf statI istype eq_stat eq_mheads
  2244        have not_static_sm: "\<not> is_static emh"
  2245          by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
  2246        from im wf dynC_Prop dynC istype statI not_static_sm
  2247        obtain dm where
  2248          "methd G dynC sig = Some dm"
  2249          "is_static dm = is_static im" 
  2250          "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
  2251          by (auto dest: implmt_methd)
  2252        with wf eq_stat resProp dynlookup eq_mheads
  2253        show ?thesis 
  2254          by (cases emh type: prod) (auto intro: widen_trans)
  2255      qed
  2256   next
  2257     case Array_Object_methd
  2258     fix T sm
  2259     assume statArr: "statT = ArrayT T" and
  2260                 sm: "accmethd G S Object sig = Some sm" and 
  2261          eq_mheads: "mhead (mthd sm) = mhd emh" 
  2262     from statArr dynC_Prop wf
  2263     have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
  2264       by (auto simp add: dynlookup_def dynmethd_C_C)
  2265     with sm eq_mheads sm 
  2266     show ?thesis 
  2267       by (cases emh type: prod) (auto dest: accmethd_SomeD)
  2268   qed
  2269 qed
  2270 declare split_paired_All [simp] split_paired_Ex [simp]
  2271 declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
  2272 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
  2273 
  2274 (* Tactical version *)
  2275 (*
  2276 lemma dynamic_mheadsD: "  
  2277  \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y;  
  2278    if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; 
  2279    isrtype G statT\<rbrakk> \<Longrightarrow>  
  2280   \<exists>m \<in> dynlookup G statT dynC sig: 
  2281      static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)"
  2282 apply (drule mheadsD)
  2283 apply safe
  2284        -- reftype statT is a class  
  2285 apply  (case_tac "\<exists>T. ClassT C = ArrayT T")
  2286 apply    (simp)
  2287 
  2288 apply    (clarsimp simp add: dynlookup_def )
  2289 apply    (frule_tac statC="C" and dynC="dynC"  and sig="sig"  
  2290          in ws_dynmethd)
  2291 apply      assumption+
  2292 apply    (case_tac "emh")  
  2293 apply    (force dest: accmethd_SomeD)
  2294 
  2295        -- reftype statT is a interface, method defined in interface 
  2296 apply    (clarsimp simp add: dynlookup_def)
  2297 apply    (drule (1) implmt_methd)
  2298 apply      blast
  2299 apply      blast
  2300 apply    (clarify)  
  2301 apply    (unfold dynimethd_def)
  2302 apply    (rule_tac x="cm" in bexI)
  2303 apply      (case_tac "emh")
  2304 apply      force
  2305 
  2306 apply      force
  2307 
  2308         -- reftype statT is a interface, method defined in Object 
  2309 apply    (simp add: dynlookup_def)
  2310 apply    (simp only: dynimethd_def)
  2311 apply    (case_tac "imethds G I sig = {}")
  2312 apply       simp
  2313 apply       (frule_tac statC="Object" and dynC="dynC"  and sig="sig"  
  2314              in ws_dynmethd)
  2315 apply          (blast intro: subcls_ObjectI wf_ws_prog) 
  2316 apply          (blast dest: class_Object)
  2317 apply       (case_tac "emh") 
  2318 apply       (force dest: accmethd_SomeD)
  2319 
  2320 apply       simp
  2321 apply       (subgoal_tac "\<exists> im. im \<in> imethds G I sig") 
  2322 prefer 2      apply blast
  2323 apply       clarify
  2324 apply       (frule (1) implmt_methd)
  2325 apply         simp
  2326 apply         blast  
  2327 apply       (clarify dest!: accmethd_SomeD)
  2328 apply       (frule (4) iface_overrides_Object)
  2329 apply       clarify
  2330 apply       (case_tac emh)
  2331 apply       force
  2332 
  2333         -- reftype statT is a array
  2334 apply    (simp add: dynlookup_def)
  2335 apply    (case_tac emh)
  2336 apply    (force dest: accmethd_SomeD simp add: dynmethd_def)
  2337 done
  2338 *)
  2339 
  2340 (* FIXME occasionally convert to ws_class_induct*) 
  2341 lemma methd_declclass:
  2342 "\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> 
  2343  \<Longrightarrow> methd G (declclass m) sig = Some m"
  2344 proof -
  2345   assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m"
  2346   have "wf_prog G  \<longrightarrow> 
  2347            (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
  2348                    \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
  2349   proof (induct G C rule: class_rec_induct', intro allI impI)
  2350     fix G C c m
  2351     assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow>
  2352                      ?P G (super c)"
  2353     assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
  2354             m: "methd G C sig = Some m"
  2355     show "methd G (declclass m) sig = Some m"
  2356     proof (cases "C=Object")
  2357       case True
  2358       with wf m show ?thesis by (auto intro: table_of_map_SomeI)
  2359     next
  2360       let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
  2361       let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
  2362       case False
  2363       with cls_C wf m
  2364       have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
  2365         by (simp add: methd_rec)
  2366       show ?thesis
  2367       proof (cases "?table sig")
  2368         case None
  2369         from this methd_C have "?filter (methd G (super c)) sig = Some m"
  2370           by simp
  2371         moreover
  2372         from wf cls_C False obtain sup where "class G (super c) = Some sup"
  2373           by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
  2374         moreover note wf False cls_C 
  2375         ultimately show ?thesis by (auto intro: hyp [rule_format])
  2376       next
  2377         case Some
  2378         from this methd_C m show ?thesis by auto 
  2379       qed
  2380     qed
  2381   qed   
  2382   with asm show ?thesis by auto
  2383 qed
  2384 
  2385 lemma dynmethd_declclass:
  2386  "\<lbrakk>dynmethd G statC dynC sig = Some m;
  2387    wf_prog G; is_class G statC
  2388   \<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m"
  2389 by (auto dest: dynmethd_declC)
  2390 
  2391 lemma dynlookup_declC:
  2392  "\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G;
  2393    is_class G dynC;isrtype G statT
  2394   \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)"
  2395 by (cases "statT")
  2396    (auto simp add: dynlookup_def dynimethd_def 
  2397              dest: methd_declC dynmethd_declC)
  2398 
  2399 lemma dynlookup_Array_declclassD [simp]:
  2400 "\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> 
  2401  \<Longrightarrow> declclass dm = Object"
  2402 proof -
  2403   assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm"
  2404   assume wf: "wf_prog G"
  2405   from wf have ws: "ws_prog G" by auto
  2406   from wf have is_cls_Obj: "is_class G Object" by auto
  2407   from dynL wf
  2408   show ?thesis
  2409     by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws]
  2410                  dest: methd_Object_SomeD)
  2411 qed   
  2412   
  2413 
  2414 declare split_paired_All [simp del] split_paired_Ex [simp del]
  2415 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
  2416 declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
  2417 
  2418 lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
  2419   dt=empty_dt \<longrightarrow> (case T of 
  2420                      Inl T \<Rightarrow> is_type (prg E) T 
  2421                    | Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))"
  2422 apply (unfold empty_dt_def)
  2423 apply (erule wt.induct)
  2424 apply (auto split del: split_if_asm simp del: snd_conv 
  2425             simp add: is_acc_class_def is_acc_type_def)
  2426 apply    (erule typeof_empty_is_type)
  2427 apply   (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], 
  2428         force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
  2429 apply  (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
  2430 apply  (drule_tac [2] accfield_fields) 
  2431 apply  (frule class_Object)
  2432 apply  (auto dest: accmethd_rT_is_type 
  2433                    imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type]
  2434              dest!:accimethdsD
  2435              simp del: class_Object
  2436              simp add: is_acc_type_def
  2437     )
  2438 done
  2439 declare split_paired_All [simp] split_paired_Ex [simp]
  2440 declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
  2441 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
  2442 
  2443 lemma ty_expr_is_type: 
  2444 "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2445 by (auto dest!: wt_is_type)
  2446 lemma ty_var_is_type: 
  2447 "\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
  2448 by (auto dest!: wt_is_type)
  2449 lemma ty_exprs_is_type: 
  2450 "\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))"
  2451 by (auto dest!: wt_is_type)
  2452 
  2453 
  2454 lemma static_mheadsD: 
  2455  "\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; 
  2456    invmode (mhd emh) e \<noteq> IntVir 
  2457   \<rbrakk> \<Longrightarrow> \<exists>m. (   (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m)
  2458                \<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> 
  2459           declrefT emh = ClassT (declclass m) \<and>  mhead (mthd m) = (mhd emh)"
  2460 apply (subgoal_tac "is_static emh \<or> e = Super")
  2461 defer apply (force simp add: invmode_def)
  2462 apply (frule  ty_expr_is_type)
  2463 apply   simp
  2464 apply (case_tac "is_static emh")
  2465 apply  (frule (1) mheadsD)
  2466 apply  clarsimp
  2467 apply  safe
  2468 apply    blast
  2469 apply   (auto dest!: imethds_wf_mhead
  2470                      accmethd_SomeD 
  2471                      accimethdsD
  2472               simp add: accObjectmheads_def Objectmheads_def)
  2473 
  2474 apply  (erule wt_elim_cases)
  2475 apply  (force simp add: cmheads_def)
  2476 done
  2477 
  2478 lemma wt_MethdI:  
  2479 "\<lbrakk>methd G C sig = Some m; wf_prog G;  
  2480   class G C = Some c\<rbrakk> \<Longrightarrow>  
  2481  \<exists>T. \<lparr>prg=G,cls=(declclass m),
  2482       lcl=callee_lcl (declclass m) sig (mthd m)\<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m"
  2483 apply (frule (2) methd_wf_mdecl, clarify)
  2484 apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
  2485 done
  2486 
  2487 subsection "accessibility concerns"
  2488 
  2489 lemma mheads_type_accessible:
  2490  "\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk>
  2491  \<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)"
  2492 by (erule mheads_cases)
  2493    (auto dest: accmethd_SomeD accessible_from_commonD accimethdsD)
  2494 
  2495 lemma static_to_dynamic_accessible_from_aux:
  2496 "\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> 
  2497  \<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC"
  2498 proof (induct rule: accessible_fromR.induct)
  2499 qed (auto intro: dyn_accessible_fromR.intros 
  2500                  member_of_to_member_in
  2501                  static_to_dynamic_overriding)
  2502 
  2503 lemma static_to_dynamic_accessible_from:
  2504   assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  2505           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2506                 wf: "wf_prog G"
  2507   shows "G\<turnstile>m in dynC dyn_accessible_from accC"
  2508 proof - 
  2509   from stat_acc subclseq 
  2510   show ?thesis (is "?Dyn_accessible m")
  2511   proof (induct rule: accessible_fromR.induct)
  2512     case (Immediate m statC)
  2513     then show "?Dyn_accessible m"
  2514       by (blast intro: dyn_accessible_fromR.Immediate
  2515                        member_inI
  2516                        permits_acc_inheritance)
  2517   next
  2518     case (Overriding m _ _)
  2519     with wf show "?Dyn_accessible m"
  2520       by (blast intro: dyn_accessible_fromR.Overriding
  2521                        member_inI
  2522                        static_to_dynamic_overriding  
  2523                        rtrancl_trancl_trancl 
  2524                        static_to_dynamic_accessible_from_aux)
  2525   qed
  2526 qed
  2527 
  2528 lemma static_to_dynamic_accessible_from_static:
  2529   assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  2530             static: "is_static m" and
  2531                 wf: "wf_prog G"
  2532   shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
  2533 proof -
  2534   from stat_acc wf 
  2535   have "G\<turnstile>m in statC dyn_accessible_from accC"
  2536     by (auto intro: static_to_dynamic_accessible_from)
  2537   from this static
  2538   show ?thesis
  2539     by (rule dyn_accessible_from_static_declC)
  2540 qed
  2541 
  2542 lemma dynmethd_member_in:
  2543   assumes    m: "dynmethd G statC dynC sig = Some m" and
  2544    iscls_statC: "is_class G statC" and
  2545             wf: "wf_prog G"
  2546   shows "G\<turnstile>Methd sig m member_in dynC"
  2547 proof -
  2548   from m 
  2549   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2550     by (auto simp add: dynmethd_def)
  2551   from subclseq iscls_statC 
  2552   have iscls_dynC: "is_class G dynC"
  2553     by (rule subcls_is_class2)
  2554   from  iscls_dynC iscls_statC wf m
  2555   have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and>
  2556         methd G (declclass m) sig = Some m" 
  2557     by - (drule dynmethd_declC, auto)
  2558   with wf 
  2559   show ?thesis
  2560     by (auto intro: member_inI dest: methd_member_of)
  2561 qed
  2562 
  2563 lemma dynmethd_access_prop:
  2564   assumes statM: "methd G statC sig = Some statM" and
  2565        stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
  2566            dynM: "dynmethd G statC dynC sig = Some dynM" and
  2567              wf: "wf_prog G" 
  2568   shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2569 proof -
  2570   from wf have ws: "ws_prog G" ..
  2571   from dynM 
  2572   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
  2573     by (auto simp add: dynmethd_def)
  2574   from stat_acc 
  2575   have is_cls_statC: "is_class G statC"
  2576     by (auto dest: accessible_from_commonD member_of_is_classD)
  2577   with subclseq 
  2578   have is_cls_dynC: "is_class G dynC"
  2579     by (rule subcls_is_class2)
  2580   from is_cls_statC statM wf 
  2581   have member_statC: "G\<turnstile>Methd sig statM member_of statC"
  2582     by (auto intro: methd_member_of)
  2583   from stat_acc 
  2584   have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)"
  2585     by (auto dest: accessible_from_commonD)
  2586   from statM subclseq is_cls_statC ws 
  2587   show ?thesis
  2588   proof (cases rule: dynmethd_cases)
  2589     case Static
  2590     assume dynmethd: "dynmethd G statC dynC sig = Some statM"
  2591     with dynM have eq_dynM_statM: "dynM=statM" 
  2592       by simp
  2593     with stat_acc subclseq wf 
  2594     show ?thesis
  2595       by (auto intro: static_to_dynamic_accessible_from)
  2596   next
  2597     case (Overrides newM)
  2598     assume dynmethd: "dynmethd G statC dynC sig = Some newM"
  2599     assume override: "G,sig\<turnstile>newM overrides statM"
  2600     assume      neq: "newM\<noteq>statM"
  2601     from dynmethd dynM 
  2602     have eq_dynM_newM: "dynM=newM" 
  2603       by simp
  2604     from dynmethd eq_dynM_newM wf is_cls_statC
  2605     have "G\<turnstile>Methd sig dynM member_in dynC"
  2606       by (auto intro: dynmethd_member_in)
  2607     moreover
  2608     from subclseq
  2609     have "G\<turnstile>dynC\<prec>\<^sub>C statC"
  2610     proof (cases rule: subclseq_cases)
  2611       case Eq
  2612       assume "dynC=statC"
  2613       moreover
  2614       from is_cls_statC obtain c
  2615         where "class G statC = Some c"
  2616         by auto
  2617       moreover 
  2618       note statM ws dynmethd 
  2619       ultimately
  2620       have "newM=statM" 
  2621         by (auto simp add: dynmethd_C_C)
  2622       with neq show ?thesis 
  2623         by (contradiction)
  2624     next
  2625       case Subcls then show ?thesis .
  2626     qed 
  2627     moreover
  2628     from stat_acc wf 
  2629     have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC"
  2630       by (blast intro: static_to_dynamic_accessible_from)
  2631     moreover
  2632     note override eq_dynM_newM
  2633     ultimately show ?thesis
  2634       by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.Overriding)
  2635   qed
  2636 qed
  2637 
  2638 lemma implmt_methd_access:
  2639   fixes accC::qtname
  2640   assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2641            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2642                isif_I: "is_iface G I" and
  2643                    wf: "wf_prog G" 
  2644   shows "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
  2645             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2646 proof -
  2647   from implements 
  2648   have iscls_dynC: "is_class G dynC" by (rule implmt_is_class)
  2649   from iface_methd
  2650   obtain im
  2651     where "im \<in> imethds G I sig"
  2652     by auto
  2653   with wf implements isif_I 
  2654   obtain dynM 
  2655     where dynM: "methd G dynC sig = Some dynM" and
  2656            pub: "accmodi dynM = Public"
  2657     by (blast dest: implmt_methd)
  2658   with iscls_dynC wf
  2659   have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2660     by (auto intro!: dyn_accessible_fromR.Immediate 
  2661               intro: methd_member_of member_of_to_member_in
  2662                      simp add: permits_acc_def)
  2663   with dynM    
  2664   show ?thesis
  2665     by blast
  2666 qed
  2667 
  2668 corollary implmt_dynimethd_access:
  2669   fixes accC::qtname
  2670   assumes iface_methd: "imethds G I sig \<noteq> {}" and
  2671            implements: "G\<turnstile>dynC\<leadsto>I"  and
  2672                isif_I: "is_iface G I" and
  2673                    wf: "wf_prog G" 
  2674   shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
  2675             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2676 proof -
  2677   from iface_methd
  2678   have "dynimethd G I dynC sig = methd G dynC sig"
  2679     by (simp add: dynimethd_def)
  2680   with iface_methd implements isif_I wf 
  2681   show ?thesis
  2682     by (simp only:)
  2683        (blast intro: implmt_methd_access)
  2684 qed
  2685 
  2686 lemma dynlookup_access_prop:
  2687   assumes emh: "emh \<in> mheads G accC statT sig" and
  2688          dynM: "dynlookup G statT dynC sig = Some dynM" and
  2689     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
  2690     isT_statT: "isrtype G statT" and
  2691            wf: "wf_prog G"
  2692   shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2693 proof -
  2694   from emh wf
  2695   have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
  2696     by (rule mheads_type_accessible)
  2697   from dynC_prop isT_statT wf
  2698   have iscls_dynC: "is_class G dynC"
  2699     by (rule valid_lookup_cls_is_class)
  2700   from emh dynC_prop isT_statT wf dynM
  2701   have eq_static: "is_static emh = is_static dynM"
  2702     by (auto dest: dynamic_mheadsD)
  2703   from emh wf show ?thesis
  2704   proof (cases rule: mheads_cases)
  2705     case (Class_methd statC _ statM)
  2706     assume statT: "statT = ClassT statC"
  2707     assume "accmethd G accC statC sig = Some statM"
  2708     then have    statM: "methd G statC sig = Some statM" and
  2709               stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC"
  2710       by (auto dest: accmethd_SomeD)
  2711     from dynM statT
  2712     have dynM': "dynmethd G statC dynC sig = Some dynM"
  2713       by (simp add: dynlookup_def) 
  2714     from statM stat_acc wf dynM'
  2715     show ?thesis
  2716       by (auto dest!: dynmethd_access_prop)
  2717   next
  2718     case (Iface_methd I im)
  2719     then have iface_methd: "imethds G I sig \<noteq> {}" and
  2720                  statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 
  2721       by (auto dest: accimethdsD)
  2722     assume   statT: "statT = IfaceT I"
  2723     assume      im: "im \<in>  accimethds G (pid accC) I sig"
  2724     assume eq_mhds: "mthd im = mhd emh"
  2725     from dynM statT
  2726     have dynM': "dynimethd G I dynC sig = Some dynM"
  2727       by (simp add: dynlookup_def)
  2728     from isT_statT statT 
  2729     have isif_I: "is_iface G I"
  2730       by simp
  2731     show ?thesis
  2732     proof (cases "is_static emh")
  2733       case False
  2734       with statT dynC_prop 
  2735       have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT"
  2736         by simp
  2737       from statT widen_dynC
  2738       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2739         by auto    
  2740       from eq_static False 
  2741       have not_static_dynM: "\<not> is_static dynM" 
  2742         by simp
  2743       from iface_methd implmnt isif_I wf dynM'
  2744       show ?thesis
  2745         by - (drule implmt_dynimethd_access, auto)
  2746     next
  2747       case True
  2748       assume "is_static emh"
  2749       moreover
  2750       from wf isT_statT statT im 
  2751       have "\<not> is_static im"
  2752         by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead)
  2753       moreover note eq_mhds
  2754       ultimately show ?thesis
  2755         by (cases emh) auto
  2756     qed
  2757   next
  2758     case (Iface_Object_methd I statM)
  2759     assume statT: "statT = IfaceT I"
  2760     assume "accmethd G accC Object sig = Some statM"
  2761     then have    statM: "methd G Object sig = Some statM" and
  2762               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2763       by (auto dest: accmethd_SomeD)
  2764     assume not_Private_statM: "accmodi statM \<noteq> Private"
  2765     assume eq_mhds: "mhead (mthd statM) = mhd emh"
  2766     from iscls_dynC wf
  2767     have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object"
  2768       by (auto intro: subcls_ObjectI)
  2769     show ?thesis
  2770     proof (cases "imethds G I sig = {}")
  2771       case True
  2772       from dynM statT True
  2773       have dynM': "dynmethd G Object dynC sig = Some dynM"
  2774         by (simp add: dynlookup_def dynimethd_def)
  2775       from statT  
  2776       have "G\<turnstile>RefT statT \<preceq>Class Object"
  2777         by auto
  2778       with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT 
  2779         wf dynM' eq_static dynC_prop  
  2780       show ?thesis
  2781         by - (drule dynmethd_access_prop,force+) 
  2782     next
  2783       case False
  2784       then obtain im where
  2785         im: "im \<in>  imethds G I sig"
  2786         by auto
  2787       have not_static_emh: "\<not> is_static emh"
  2788       proof -
  2789         from im statM statT isT_statT wf not_Private_statM 
  2790         have "is_static im = is_static statM"
  2791           by (fastforce dest: wf_imethds_hiding_objmethdsD)
  2792         with wf isT_statT statT im 
  2793         have "\<not> is_static statM"
  2794           by (auto dest: wf_prog_idecl imethds_wf_mhead)
  2795         with eq_mhds
  2796         show ?thesis  
  2797           by (cases emh) auto
  2798       qed
  2799       with statT dynC_prop
  2800       have implmnt: "G\<turnstile>dynC\<leadsto>I"
  2801         by simp
  2802       with isT_statT statT
  2803       have isif_I: "is_iface G I"
  2804         by simp
  2805       from dynM statT
  2806       have dynM': "dynimethd G I dynC sig = Some dynM"
  2807         by (simp add: dynlookup_def) 
  2808       from False implmnt isif_I wf dynM'
  2809       show ?thesis
  2810         by - (drule implmt_dynimethd_access, auto)
  2811     qed
  2812   next
  2813     case (Array_Object_methd T statM)
  2814     assume statT: "statT = ArrayT T"
  2815     assume "accmethd G accC Object sig = Some statM"
  2816     then have    statM: "methd G Object sig = Some statM" and
  2817               stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC"
  2818       by (auto dest: accmethd_SomeD)
  2819     from statT dynC_prop
  2820     have dynC_Obj: "dynC = Object" 
  2821       by simp
  2822     then
  2823     have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object"
  2824       by simp
  2825     from dynM statT    
  2826     have dynM': "dynmethd G Object dynC sig = Some dynM"
  2827       by (simp add: dynlookup_def)
  2828     from statM statT_acc stat_acc dynM' wf widen_dynC_Obj  
  2829          statT isT_statT  
  2830     show ?thesis   
  2831       by - (drule dynmethd_access_prop, simp+) 
  2832   qed
  2833 qed
  2834 
  2835 lemma dynlookup_access:
  2836   assumes emh: "emh \<in> mheads G accC statT sig" and
  2837     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
  2838     isT_statT: "isrtype G statT" and
  2839            wf: "wf_prog G"
  2840   shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
  2841             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
  2842 proof - 
  2843   from dynC_prop isT_statT wf
  2844   have is_cls_dynC: "is_class G dynC"
  2845     by (auto dest: valid_lookup_cls_is_class)
  2846   with emh wf dynC_prop isT_statT
  2847   obtain dynM where 
  2848     "dynlookup G statT dynC sig = Some dynM"
  2849     by - (drule dynamic_mheadsD,auto)
  2850   with  emh dynC_prop isT_statT wf
  2851   show ?thesis 
  2852     by (blast intro: dynlookup_access_prop)
  2853 qed
  2854 
  2855 lemma stat_overrides_Package_old: 
  2856   assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
  2857           accmodi_new: "accmodi new = Package" and
  2858                    wf: "wf_prog G "
  2859   shows "accmodi old = Package"
  2860 proof -
  2861   from stat_override wf 
  2862   have "accmodi old \<le> accmodi new"
  2863     by (auto dest: wf_prog_stat_overridesD)
  2864   with stat_override accmodi_new show ?thesis
  2865     by (cases "accmodi old") (auto dest: no_Private_stat_override 
  2866                                    dest: acc_modi_le_Dests)
  2867 qed
  2868 
  2869 subsubsection {* Properties of dynamic accessibility *}
  2870 
  2871 lemma dyn_accessible_Private:
  2872  assumes dyn_acc: "G \<turnstile> m in C dyn_accessible_from accC" and
  2873             priv: "accmodi m = Private"
  2874    shows "accC = declclass m"
  2875 proof -
  2876   from dyn_acc priv
  2877   show ?thesis
  2878   proof (induct)
  2879     case (Immediate m C)
  2880     from `G \<turnstile> m in C permits_acc_from accC` and `accmodi m = Private`
  2881     show ?case
  2882       by (simp add: permits_acc_def)
  2883   next
  2884     case Overriding
  2885     then show ?case
  2886       by (auto dest!: overrides_commonD)
  2887   qed
  2888 qed
  2889 
  2890 text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. 
  2891 Without it. it is easy to leaf the Package!
  2892 *}
  2893 lemma dyn_accessible_Package:
  2894  "\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package;
  2895    wf_prog G\<rbrakk>
  2896   \<Longrightarrow> pid accC = pid (declclass m)"
  2897 proof -
  2898   assume wf: "wf_prog G "
  2899   assume accessible: "G \<turnstile> m in C dyn_accessible_from accC"
  2900   then show "accmodi m = Package 
  2901             \<Longrightarrow> pid accC = pid (declclass m)"
  2902     (is "?Pack m \<Longrightarrow> ?P m")
  2903   proof (induct rule: dyn_accessible_fromR.induct)
  2904     case (Immediate m C)
  2905     assume "G\<turnstile>m member_in C"
  2906            "G \<turnstile> m in C permits_acc_from accC"
  2907            "accmodi m = Package"      
  2908     then show "?P m"
  2909       by (auto simp add: permits_acc_def)
  2910   next
  2911     case (Overriding new declC newm old Sup C)
  2912     assume member_new: "G \<turnstile> new member_in C" and
  2913                   new: "new = (declC, mdecl newm)" and
  2914              override: "G \<turnstile> (declC, newm) overrides old" and
  2915          subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
  2916               acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and
  2917                   hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and
  2918           accmodi_new: "accmodi new = Package"
  2919     from override accmodi_new new wf 
  2920     have accmodi_old: "accmodi old = Package"  
  2921       by (auto dest: overrides_Package_old)
  2922     with hyp 
  2923     have P_sup: "?P (methdMembr old)"
  2924       by (simp)
  2925     from wf override new accmodi_old accmodi_new
  2926     have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
  2927       by (auto dest: dyn_override_Package)
  2928     with eq_pid_new_old P_sup show "?P new"
  2929       by auto
  2930   qed
  2931 qed
  2932 
  2933 text {* For fields we don't need the wellformedness of the program, since
  2934 there is no overriding *}
  2935 lemma dyn_accessible_field_Package:
  2936  assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
  2937             pack: "accmodi f = Package" and
  2938            field: "is_field f"
  2939    shows "pid accC = pid (declclass f)"
  2940 proof -
  2941   from dyn_acc pack field
  2942   show ?thesis
  2943   proof (induct)
  2944     case (Immediate f C)
  2945     from `G \<turnstile> f in C permits_acc_from accC` and `accmodi f = Package`
  2946     show ?case
  2947       by (simp add: permits_acc_def)
  2948   next
  2949     case Overriding
  2950     then show ?case by (simp add: is_field_def)
  2951   qed
  2952 qed
  2953 
  2954 text {* @{text dyn_accessible_instance_field_Protected} only works for fields
  2955 since methods can break the package bounds due to overriding
  2956 *}
  2957 lemma dyn_accessible_instance_field_Protected:
  2958   assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
  2959              prot: "accmodi f = Protected" and
  2960             field: "is_field f" and
  2961    instance_field: "\<not> is_static f" and
  2962           outside: "pid (declclass f) \<noteq> pid accC"
  2963   shows "G\<turnstile> C \<preceq>\<^sub>C accC"
  2964 proof -
  2965   from dyn_acc prot field instance_field outside
  2966   show ?thesis
  2967   proof (induct)
  2968     case (Immediate f C)
  2969     note `G \<turnstile> f in C permits_acc_from accC`
  2970     moreover 
  2971     assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
  2972            "pid (declclass f) \<noteq> pid accC"
  2973     ultimately 
  2974     show "G\<turnstile> C \<preceq>\<^sub>C accC"
  2975       by (auto simp add: permits_acc_def)
  2976   next
  2977     case Overriding
  2978     then show ?case by (simp add: is_field_def)
  2979   qed
  2980 qed
  2981    
  2982 lemma dyn_accessible_static_field_Protected:
  2983   assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
  2984              prot: "accmodi f = Protected" and
  2985             field: "is_field f" and
  2986      static_field: "is_static f" and
  2987           outside: "pid (declclass f) \<noteq> pid accC"
  2988   shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
  2989 proof -
  2990   from dyn_acc prot field static_field outside
  2991   show ?thesis
  2992   proof (induct)
  2993     case (Immediate f C)
  2994     assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
  2995            "pid (declclass f) \<noteq> pid accC"
  2996     moreover
  2997     note `G \<turnstile> f in C permits_acc_from accC`
  2998     ultimately
  2999     have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
  3000       by (auto simp add: permits_acc_def)
  3001     moreover
  3002     from `G \<turnstile> f member_in C`
  3003     have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
  3004       by (rule member_in_class_relation)
  3005     ultimately show ?case
  3006       by blast
  3007   next
  3008     case Overriding
  3009     then show ?case by (simp add: is_field_def)
  3010   qed
  3011 qed
  3012 
  3013 end