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