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