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