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