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