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