src/HOL/Bali/DeclConcepts.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32754 4e0256f7d219
child 34915 7894c7dab132
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  Title:      HOL/Bali/DeclConcepts.thy
     2     ID:         $Id$
     3     Author:     Norbert Schirmer
     4 *)
     5 header {* Advanced concepts on Java declarations like overriding, inheritance,
     6 dynamic method lookup*}
     7 
     8 theory DeclConcepts imports TypeRel begin
     9 
    10 section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
    11 
    12 constdefs
    13 is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
    14 "is_public G qn \<equiv> (case class G qn of
    15                      None       \<Rightarrow> (case iface G qn of
    16                                       None       \<Rightarrow> False
    17                                     | Some iface \<Rightarrow> access iface = Public)
    18                    | Some class \<Rightarrow> access class = Public)"
    19 
    20 subsection "accessibility of types (cf. 6.6.1)"
    21 text {* 
    22 Primitive types are always accessible, interfaces and classes are accessible
    23 in their package or if they are defined public, an array type is accessible if
    24 its element type is accessible *}
    25  
    26 consts accessible_in   :: "prog \<Rightarrow> ty     \<Rightarrow> pname \<Rightarrow> bool"  
    27                                       ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
    28        rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 
    29                                       ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 
    30 primrec
    31 "G\<turnstile>(PrimT p)   accessible_in pack  = True"
    32 accessible_in_RefT_simp: 
    33 "G\<turnstile>(RefT  r)   accessible_in pack  = G\<turnstile>r accessible_in' pack"
    34 
    35 "G\<turnstile>(NullT)     accessible_in' pack = True"
    36 "G\<turnstile>(IfaceT I)  accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
    37 "G\<turnstile>(ClassT C)  accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
    38 "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
    39 
    40 declare accessible_in_RefT_simp [simp del]
    41 
    42 constdefs
    43   is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    44     "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    45   is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
    46     "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
    47   is_acc_type  :: "prog \<Rightarrow> pname \<Rightarrow> ty     \<Rightarrow> bool"
    48     "is_acc_type  G P T \<equiv> is_type G T  \<and> G\<turnstile>T accessible_in P"
    49   is_acc_reftype  :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
    50   "is_acc_reftype  G P T \<equiv> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
    51 
    52 lemma is_acc_classD:
    53  "is_acc_class G P C \<Longrightarrow>  is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
    54 by (simp add: is_acc_class_def)
    55 
    56 lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C"
    57 by (auto simp add: is_acc_class_def)
    58 
    59 lemma is_acc_ifaceD:
    60   "is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
    61 by (simp add: is_acc_iface_def)
    62 
    63 lemma is_acc_typeD:
    64  "is_acc_type  G P T \<Longrightarrow> is_type G T  \<and> G\<turnstile>T accessible_in P"
    65 by (simp add: is_acc_type_def)
    66 
    67 lemma is_acc_reftypeD:
    68 "is_acc_reftype  G P T \<Longrightarrow> isrtype G T  \<and> G\<turnstile>T accessible_in' P"
    69 by (simp add: is_acc_reftype_def)
    70 
    71 subsection "accessibility of members"
    72 text {*
    73 The accessibility of members is more involved as the accessibility of types.
    74 We have to distinguish several cases to model the different effects of 
    75 accessibility during inheritance, overriding and ordinary member access 
    76 *}
    77 
    78 subsubsection {* Various technical conversion and selection functions *}
    79 
    80 text {* overloaded selector @{text accmodi} to select the access modifier 
    81 out of various HOL types *}
    82 
    83 axclass has_accmodi < "type"
    84 consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
    85 
    86 instance acc_modi::has_accmodi ..
    87 
    88 defs (overloaded)
    89 acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    90 
    91 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    92 by (simp add: acc_modi_accmodi_def)
    93 
    94 instance decl_ext_type:: ("type") has_accmodi ..
    95 
    96 defs (overloaded)
    97 decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    98 
    99 
   100 lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
   101 by (simp add: decl_acc_modi_def)
   102 
   103 instance * :: ("type",has_accmodi) has_accmodi ..
   104 
   105 defs (overloaded)
   106 pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
   107 
   108 lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
   109 by (simp add: pair_acc_modi_def)
   110 
   111 instance memberdecl :: has_accmodi ..
   112 
   113 defs (overloaded)
   114 memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
   115                                           fdecl f \<Rightarrow> accmodi f
   116                                         | mdecl m \<Rightarrow> accmodi m)"
   117 
   118 lemma memberdecl_fdecl_acc_modi_simp[simp]:
   119  "accmodi (fdecl m) = accmodi m"
   120 by (simp add: memberdecl_acc_modi_def)
   121 
   122 lemma memberdecl_mdecl_acc_modi_simp[simp]:
   123  "accmodi (mdecl m) = accmodi m"
   124 by (simp add: memberdecl_acc_modi_def)
   125 
   126 text {* overloaded selector @{text declclass} to select the declaring class 
   127 out of various HOL types *}
   128 
   129 axclass has_declclass < "type"
   130 consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
   131 
   132 instance qtname_ext_type::("type") has_declclass ..
   133 
   134 defs (overloaded)
   135 qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
   136 
   137 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
   138 by (simp add: qtname_declclass_def)
   139 
   140 instance * :: ("has_declclass","type") has_declclass ..
   141 
   142 defs (overloaded)
   143 pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   144 
   145 lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
   146 by (simp add: pair_declclass_def)
   147 
   148 text {* overloaded selector @{text is_static} to select the static modifier 
   149 out of various HOL types *}
   150 
   151 
   152 axclass has_static < "type"
   153 consts is_static :: "'a::has_static \<Rightarrow> bool"
   154 
   155 instance decl_ext_type :: ("has_static") has_static ..
   156 
   157 instance member_ext_type :: ("type") has_static ..
   158 
   159 defs (overloaded)
   160 static_field_type_is_static_def: 
   161  "is_static (m::('b member_scheme)) \<equiv> static m"
   162 
   163 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
   164 by (simp add: static_field_type_is_static_def)
   165 
   166 instance * :: ("type","has_static") has_static ..
   167 
   168 defs (overloaded)
   169 pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   170 
   171 lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
   172 by (simp add: pair_is_static_def)
   173 
   174 lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
   175 by (simp add: pair_is_static_def)
   176 
   177 instance memberdecl:: has_static ..
   178 
   179 defs (overloaded)
   180 memberdecl_is_static_def: 
   181  "is_static m \<equiv> (case m of
   182                     fdecl f \<Rightarrow> is_static f
   183                   | mdecl m \<Rightarrow> is_static m)"
   184 
   185 lemma memberdecl_is_static_fdecl_simp[simp]:
   186  "is_static (fdecl f) = is_static f"
   187 by (simp add: memberdecl_is_static_def)
   188 
   189 lemma memberdecl_is_static_mdecl_simp[simp]:
   190  "is_static (mdecl m) = is_static m"
   191 by (simp add: memberdecl_is_static_def)
   192 
   193 lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
   194 by (cases m) (simp add: mhead_def member_is_static_simp)
   195 
   196 constdefs  --{* some mnemotic selectors for various pairs *} 
   197            
   198  "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
   199  "decliface \<equiv> fst"          --{* get the interface component *}
   200 
   201  "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
   202  "mbr \<equiv> snd"            --{* get the memberdecl component *}
   203 
   204  "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
   205                            --{* also used for mdecl, mhead *}
   206  "mthd \<equiv> snd"              --{* get the method component *}
   207 
   208  "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
   209               --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
   210  "fld \<equiv> snd"               --{* get the field component *}
   211 
   212 
   213 constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
   214  fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
   215  "fname \<equiv> fst"
   216   
   217   declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
   218  "declclassf \<equiv> snd"
   219 
   220 
   221 
   222 lemma decliface_simp[simp]: "decliface (I,m) = I"
   223 by (simp add: decliface_def) 
   224 
   225 lemma mbr_simp[simp]: "mbr (C,m) = m"
   226 by (simp add: mbr_def)
   227 
   228 lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m"
   229 by (cases m) (simp add:  mbr_def) 
   230 
   231 lemma mthd_simp[simp]: "mthd (C,m) = m"
   232 by (simp add: mthd_def)
   233 
   234 lemma fld_simp[simp]: "fld (C,f) = f"
   235 by (simp add: fld_def)
   236 
   237 lemma accmodi_simp[simp]: "accmodi (C,m) = access m"
   238 by (simp )
   239 
   240 lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m"
   241 by (cases m) (simp add: mthd_def) 
   242 
   243 lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
   244 by (cases f) (simp add:  fld_def) 
   245 
   246 lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
   247 by (cases m) (simp add:  mthd_def member_is_static_simp)
   248 
   249 lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m"
   250 by (cases m) simp
   251 
   252 lemma static_fld_simp[simp]: "static (fld f) = is_static f"
   253 by (cases f) (simp add:  fld_def member_is_static_simp)
   254 
   255 lemma ext_field_simp [simp]: "(declclass f,fld f) = f"
   256 by (cases f) (simp add:  fld_def)
   257 
   258 lemma ext_method_simp [simp]: "(declclass m,mthd m) = m"
   259 by (cases m) (simp add:  mthd_def)
   260 
   261 lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m"
   262 by (cases m) (simp add: mbr_def)
   263 
   264 lemma fname_simp[simp]:"fname (n,c) = n"
   265 by (simp add: fname_def)
   266 
   267 lemma declclassf_simp[simp]:"declclassf (n,c) = c"
   268 by (simp add: declclassf_def)
   269 
   270 constdefs  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
   271   "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
   272   "fldname \<equiv> fst"
   273 
   274   "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
   275   "fldclass \<equiv> snd"
   276 
   277 lemma fldname_simp[simp]: "fldname (n,c) = n"
   278 by (simp add: fldname_def)
   279 
   280 lemma fldclass_simp[simp]: "fldclass (n,c) = c"
   281 by (simp add: fldclass_def)
   282 
   283 lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
   284 by (simp add: fldname_def fldclass_def)
   285 
   286 text {* Convert a qualified method declaration (qualified with its declaring 
   287 class) to a qualified member declaration:  @{text methdMembr}  *}
   288 
   289 constdefs
   290 methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)"
   291  "methdMembr m \<equiv> (fst m,mdecl (snd m))"
   292 
   293 lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
   294 by (simp add: methdMembr_def)
   295 
   296 lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m"
   297 by (cases m) (simp add: methdMembr_def)
   298 
   299 lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m"
   300 by (cases m) (simp add: methdMembr_def)
   301 
   302 lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
   303 by (cases m) (simp add: methdMembr_def)
   304 
   305 text {* Convert a qualified method (qualified with its declaring 
   306 class) to a qualified member declaration:  @{text method}  *}
   307 
   308 constdefs
   309 method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 
   310 "method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
   311 
   312 lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
   313 by (simp add: method_def)
   314 
   315 lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m"
   316 by (simp add: method_def)
   317 
   318 lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m"
   319 by (simp add: method_def)
   320 
   321 lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m"
   322 by (cases m) (simp add: method_def)
   323 
   324 lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)"
   325 by (simp add: mbr_def method_def)
   326 
   327 lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
   328   by (simp add: method_def) 
   329 
   330 constdefs
   331 fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 
   332 "fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
   333 
   334 lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
   335 by (simp add: fieldm_def)
   336 
   337 lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f"
   338 by (simp add: fieldm_def)
   339 
   340 lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f"
   341 by (simp add: fieldm_def)
   342 
   343 lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f"
   344 by (cases f) (simp add: fieldm_def)
   345 
   346 lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)"
   347 by (simp add: mbr_def fieldm_def)
   348 
   349 lemma memberid_fieldm_simp[simp]:  "memberid (fieldm n f) = fid n"
   350 by (simp add: fieldm_def) 
   351 
   352 text {* Select the signature out of a qualified method declaration:
   353  @{text msig} *}
   354 
   355 constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig"
   356 "msig m \<equiv> fst (snd m)"
   357 
   358 lemma msig_simp[simp]: "msig (c,(s,m)) = s"
   359 by (simp add: msig_def)
   360 
   361 text {* Convert a qualified method (qualified with its declaring 
   362 class) to a qualified method declaration:  @{text qmdecl}  *}
   363 
   364 constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
   365 "qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
   366 
   367 lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
   368 by (simp add: qmdecl_def)
   369 
   370 lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m"
   371 by (simp add: qmdecl_def)
   372 
   373 lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m"
   374 by (simp add: qmdecl_def)
   375 
   376 lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m"
   377 by (cases m) (simp add: qmdecl_def)
   378 
   379 lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig"
   380 by (simp add: qmdecl_def)
   381 
   382 lemma mdecl_qmdecl_simp[simp]:  
   383  "mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 
   384 by (simp add: qmdecl_def) 
   385 
   386 lemma methdMembr_qmdecl_simp [simp]: 
   387  "methdMembr (qmdecl sig old) = method sig old"
   388 by (simp add: methdMembr_def qmdecl_def method_def)
   389 
   390 text {* overloaded selector @{text resTy} to select the result type 
   391 out of various HOL types *}
   392 
   393 axclass has_resTy < "type"
   394 consts resTy:: "'a::has_resTy \<Rightarrow> ty"
   395 
   396 instance decl_ext_type :: ("has_resTy") has_resTy ..
   397 
   398 instance member_ext_type :: ("has_resTy") has_resTy ..
   399 
   400 instance mhead_ext_type :: ("type") has_resTy ..
   401 
   402 defs (overloaded)
   403 mhead_ext_type_resTy_def: 
   404  "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   405 
   406 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
   407 by (simp add: mhead_ext_type_resTy_def)
   408 
   409 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   410 by (simp add: mhead_def mhead_resTy_simp)
   411 
   412 instance * :: ("type","has_resTy") has_resTy ..
   413 
   414 defs (overloaded)
   415 pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   416 
   417 lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
   418 by (simp add: pair_resTy_def)
   419 
   420 lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m"
   421 by (cases m) (simp)
   422 
   423 lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m"
   424 by (cases m) (simp add: mthd_def )
   425 
   426 subsubsection "inheritable-in"
   427 text {*
   428 @{text "G\<turnstile>m inheritable_in P"}: m can be inherited by
   429 classes in package P if:
   430 \begin{itemize} 
   431 \item the declaration class of m is accessible in P and
   432 \item the member m is declared with protected or public access or if it is
   433       declared with default (package) access, the package of the declaration 
   434       class of m is also P. If the member m is declared with private access
   435       it is not accessible for inheritance at all.
   436 \end{itemize}
   437 *}
   438 constdefs
   439 inheritable_in:: 
   440  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool"
   441                   ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
   442 "G\<turnstile>membr inheritable_in pack 
   443   \<equiv> (case (accmodi membr) of
   444        Private   \<Rightarrow> False
   445      | Package   \<Rightarrow> (pid (declclass membr)) = pack
   446      | Protected \<Rightarrow> True
   447      | Public    \<Rightarrow> True)"
   448 
   449 syntax
   450 Method_inheritable_in::
   451  "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool"
   452                 ("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60)
   453 
   454 translations
   455 "G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p"
   456 
   457 syntax
   458 Methd_inheritable_in::
   459  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool"
   460                 ("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
   461 
   462 translations
   463 "G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p"
   464 
   465 subsubsection "declared-in/undeclared-in"
   466 
   467 constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table"
   468 "cdeclaredmethd G C 
   469   \<equiv> (case class G C of
   470        None \<Rightarrow> \<lambda> sig. None
   471      | Some c \<Rightarrow> table_of (methods c)
   472     )"
   473 
   474 constdefs
   475 cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table"
   476 "cdeclaredfield G C 
   477   \<equiv> (case class G C of
   478        None \<Rightarrow> \<lambda> sig. None
   479      | Some c \<Rightarrow> table_of (cfields c)
   480     )"
   481 
   482 
   483 constdefs
   484 declared_in:: "prog  \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool"
   485                                  ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
   486 "G\<turnstile>m declared_in C \<equiv> (case m of
   487                         fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn  = Some f
   488                       | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
   489 
   490 syntax
   491 method_declared_in:: "prog  \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   492                                  ("_\<turnstile>Method _ declared'_in _" [61,61,61] 60)
   493 translations
   494 "G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C"
   495 
   496 syntax
   497 methd_declared_in:: "prog  \<Rightarrow> sig  \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   498                                ("_\<turnstile>Methd _  _ declared'_in _" [61,61,61,61] 60)
   499 translations
   500 "G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C"
   501 
   502 lemma declared_in_classD:
   503  "G\<turnstile>m declared_in C \<Longrightarrow> is_class G C"
   504 by (cases m) 
   505    (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   506 
   507 constdefs
   508 undeclared_in:: "prog  \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool"
   509                                  ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
   510 
   511 "G\<turnstile>m undeclared_in C \<equiv> (case m of
   512                             fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
   513                           | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
   514 
   515 
   516 subsubsection "members"
   517 
   518 (* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because
   519    the class qtname changes to the superclass in the inductive definition
   520    below
   521 *)
   522 
   523 inductive
   524   members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   525     ("_ \<turnstile> _ member'_of _" [61,61,61] 60)
   526   for G :: prog
   527 where
   528 
   529   Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
   530 | Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 
   531                G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 
   532               \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
   533 text {* Note that in the case of an inherited member only the members of the
   534 direct superclass are concerned. If a member of a superclass of the direct
   535 superclass isn't inherited in the direct superclass (not member of the
   536 direct superclass) than it can't be a member of the class. E.g. If a
   537 member of a class A is defined with package access it isn't member of a 
   538 subclass S if S isn't in the same package as A. Any further subclasses 
   539 of S will not inherit the member, regardless if they are in the same
   540 package as A or not.*}
   541 
   542 syntax
   543 method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   544                            ("_ \<turnstile>Method _ member'_of _" [61,61,61] 60)
   545 
   546 translations
   547  "G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 
   548 
   549 syntax
   550 methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   551                            ("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60)
   552 
   553 translations
   554  "G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 
   555 
   556 syntax
   557 fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool"
   558                            ("_ \<turnstile>Field _  _ member'_of _" [61,61,61] 60)
   559 
   560 translations
   561  "G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 
   562 
   563 constdefs
   564 inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool"
   565                            ("_ \<turnstile> _ inherits _" [61,61,61] 60)
   566 "G\<turnstile>C inherits m 
   567   \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 
   568     (\<exists> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
   569 
   570 lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
   571 by (auto simp add: inherits_def intro: members.Inherited)
   572 
   573 
   574 constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   575                            ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
   576 "G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   577 text {* A member is in a class if it is member of the class or a superclass.
   578 If a member is in a class we can select this member. This additional notion
   579 is necessary since not all members are inherited to subclasses. So such
   580 members are not member-of the subclass but member-in the subclass.*}
   581 
   582 syntax
   583 method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   584                            ("_ \<turnstile>Method _ member'_in _" [61,61,61] 60)
   585 
   586 translations
   587  "G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 
   588 
   589 syntax
   590 methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool"
   591                            ("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60)
   592 
   593 translations
   594  "G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 
   595 
   596 lemma member_inD: "G\<turnstile>m member_in C 
   597  \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
   598 by (auto simp add: member_in_def)
   599 
   600 lemma member_inI: "\<lbrakk>G \<turnstile> m member_of provC;G\<turnstile> C \<preceq>\<^sub>C provC\<rbrakk> \<Longrightarrow>  G\<turnstile>m member_in C"
   601 by (auto simp add: member_in_def)
   602 
   603 lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C"
   604 by (auto intro: member_inI)
   605 
   606 
   607 subsubsection "overriding"
   608 
   609 text {* Unfortunately the static notion of overriding (used during the
   610 typecheck of the compiler) and the dynamic notion of overriding (used during
   611 execution in the JVM) are not exactly the same. 
   612 *}
   613 
   614 text {* Static overriding (used during the typecheck of the compiler) *}
   615 
   616 inductive
   617   stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
   618     ("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
   619   for G :: prog
   620 where
   621 
   622   Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 
   623            G\<turnstile>Method new declared_in (declclass new);  
   624            G\<turnstile>Method old declared_in (declclass old); 
   625            G\<turnstile>Method old inheritable_in pid (declclass new);
   626            G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew;
   627            G \<turnstile>Method old member_of superNew
   628            \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
   629 
   630 | Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
   631              \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
   632 
   633 text {* Dynamic overriding (used during the typecheck of the compiler) *}
   634 
   635 inductive
   636   overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
   637     ("_ \<turnstile> _ overrides _" [61,61,61] 60)
   638   for G :: prog
   639 where
   640 
   641   Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private;
   642            msig new = msig old; 
   643            G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
   644            G\<turnstile>Method new declared_in (declclass new);  
   645            G\<turnstile>Method old declared_in (declclass old);    
   646            G\<turnstile>Method old inheritable_in pid (declclass new);
   647            G\<turnstile>resTy new \<preceq> resTy old
   648            \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
   649 
   650 | Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
   651             \<Longrightarrow> G\<turnstile>new overrides old"
   652 
   653 syntax
   654 sig_stat_overrides:: 
   655  "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   656                                   ("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60)
   657 translations
   658  "G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 
   659 
   660 syntax
   661 sig_overrides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 
   662                                   ("_,_\<turnstile> _ overrides _" [61,61,61,61] 60)
   663 translations
   664  "G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 
   665 
   666 subsubsection "Hiding"
   667 
   668 constdefs hides::
   669 "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
   670                                 ("_\<turnstile> _ hides _" [61,61,61] 60)
   671 "G\<turnstile>new hides old
   672   \<equiv> is_static new \<and> msig new = msig old \<and>
   673     G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   674     G\<turnstile>Method new declared_in (declclass new) \<and>
   675     G\<turnstile>Method old declared_in (declclass old) \<and> 
   676     G\<turnstile>Method old inheritable_in pid (declclass new)"
   677 
   678 syntax
   679 sig_hides:: "prog  \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 
   680                                   ("_,_\<turnstile> _ hides _" [61,61,61,61] 60)
   681 translations
   682  "G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 
   683 
   684 lemma hidesI:
   685 "\<lbrakk>is_static new; msig new = msig old;
   686   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old);
   687   G\<turnstile>Method new declared_in (declclass new);
   688   G\<turnstile>Method old declared_in (declclass old);
   689   G\<turnstile>Method old inheritable_in pid (declclass new)
   690  \<rbrakk> \<Longrightarrow> G\<turnstile>new hides old"
   691 by (auto simp add: hides_def)
   692 
   693 lemma hidesD:
   694 "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow>  
   695   declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 
   696   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   697   G\<turnstile>Method new declared_in (declclass new) \<and>   
   698   G\<turnstile>Method old declared_in (declclass old)"
   699 by (auto simp add: hides_def)
   700 
   701 lemma overrides_commonD:
   702 "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow>  
   703   declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
   704   accmodi new \<noteq> Private \<and> 
   705   msig new = msig old  \<and>
   706   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   707   G\<turnstile>Method new declared_in (declclass new) \<and>   
   708   G\<turnstile>Method old declared_in (declclass old)"
   709 by (induct set: overridesR) (auto intro: trancl_trans)
   710 
   711 lemma ws_overrides_commonD:
   712 "\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow>  
   713   declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and>
   714   accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and>
   715   msig new = msig old  \<and>
   716   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
   717   G\<turnstile>Method new declared_in (declclass new) \<and>   
   718   G\<turnstile>Method old declared_in (declclass old)"
   719 by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)
   720 
   721 lemma overrides_eq_sigD: 
   722  "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new"
   723 by (auto dest: overrides_commonD)
   724 
   725 lemma hides_eq_sigD: 
   726  "\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new"
   727 by (auto simp add: hides_def)
   728 
   729 subsubsection "permits access" 
   730 constdefs 
   731 permits_acc:: 
   732  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   733                    ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
   734 
   735 "G\<turnstile>membr in class permits_acc_from accclass 
   736   \<equiv> (case (accmodi membr) of
   737        Private   \<Rightarrow> (declclass membr = accclass)
   738      | Package   \<Rightarrow> (pid (declclass membr) = pid accclass)
   739      | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
   740                     \<or>
   741                     (G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
   742                      \<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
   743      | Public    \<Rightarrow> True)"
   744 text {*
   745 The subcondition of the @{term "Protected"} case: 
   746 @{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
   747 @{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the
   748 same the other condition @{term "(pid (declclass membr) = pid accclass)"}
   749 holds anyway.
   750 *} 
   751 
   752 text {* Like in case of overriding, the static and dynamic accessibility 
   753 of members is not uniform.
   754 \begin{itemize}
   755 \item Statically the class/interface of the member must be accessible for the
   756       member to be accessible. During runtime this is not necessary. For
   757       Example, if a class is accessible and we are allowed to access a member
   758       of this class (statically) we expect that we can access this member in 
   759       an arbitrary subclass (during runtime). It's not intended to restrict
   760       the access to accessible subclasses during runtime.
   761 \item Statically the member we want to access must be "member of" the class.
   762       Dynamically it must only be "member in" the class.
   763 \end{itemize} 
   764 *} 
   765 
   766 inductive
   767   accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   768   and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   769     ("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
   770   and method_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   771     ("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60)
   772   for G :: prog and accclass :: qtname
   773 where
   774   "G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls"
   775 
   776 | "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
   777 
   778 | Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
   779                 G\<turnstile>(Class class) accessible_in (pid accclass);
   780                 G\<turnstile>membr in class permits_acc_from accclass 
   781                \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   782 
   783 | Overriding: "\<lbrakk>G\<turnstile>membr member_of class;
   784                 G\<turnstile>(Class class) accessible_in (pid accclass);
   785                 membr=(C,mdecl new);
   786                 G\<turnstile>(C,new) overrides\<^sub>S old; 
   787                 G\<turnstile>class \<prec>\<^sub>C supr;
   788                 G\<turnstile>Method old of supr accessible_from accclass
   789                \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
   790 
   791 syntax 
   792 methd_accessible_from:: 
   793  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   794                  ("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
   795 
   796 translations
   797 "G\<turnstile>Methd s m of cls accessible_from accclass"  
   798  \<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass"  
   799 
   800 syntax 
   801 field_accessible_from:: 
   802  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   803                  ("_ \<turnstile>Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
   804 
   805 translations
   806 "G\<turnstile>Field fn f of C accessible_from accclass"  
   807  \<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 
   808 
   809 inductive
   810   dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
   811   and dyn_accessible_from' ::  "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   812     ("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   813   and method_dyn_accessible_from :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   814     ("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
   815   for G :: prog and accclass :: qtname
   816 where
   817   "G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C"
   818 
   819 | "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
   820 
   821 | Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
   822                 G\<turnstile>membr in class permits_acc_from accclass 
   823                \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   824 
   825 | Overriding: "\<lbrakk>G\<turnstile>membr member_in class;
   826                 membr=(C,mdecl new);
   827                 G\<turnstile>(C,new) overrides old; 
   828                 G\<turnstile>class \<prec>\<^sub>C supr;
   829                 G\<turnstile>Method old in supr dyn_accessible_from accclass
   830                \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
   831 
   832 syntax 
   833 methd_dyn_accessible_from:: 
   834  "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   835              ("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   836 
   837 translations
   838 "G\<turnstile>Methd s m in C dyn_accessible_from accC"  
   839  \<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC"  
   840 
   841 syntax 
   842 field_dyn_accessible_from:: 
   843  "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
   844          ("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
   845 
   846 translations
   847 "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"  
   848  \<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
   849 
   850 
   851 lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S
   852  \<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)"
   853 by (auto elim: accessible_fromR.induct)
   854 
   855 lemma unique_declaration: 
   856  "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
   857   \<Longrightarrow> m = n"
   858 apply (cases m)
   859 apply (cases n,
   860         auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
   861 done
   862 
   863 lemma declared_not_undeclared:
   864   "G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C"
   865 by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   866 
   867 lemma undeclared_not_declared:
   868  "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
   869 by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   870 
   871 lemma not_undeclared_declared:
   872   "\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 
   873                                            membr_id = memberid m)"
   874 proof -
   875   assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C"
   876   show ?thesis (is "?P membr_id")
   877   proof (cases membr_id)
   878     case (fid vname)
   879     with not_undecl
   880     obtain fld where
   881       "G\<turnstile>fdecl (vname,fld) declared_in C" 
   882       by (auto simp add: undeclared_in_def declared_in_def
   883                          cdeclaredfield_def)
   884     with fid show ?thesis 
   885       by auto
   886   next
   887     case (mid sig)
   888     with not_undecl
   889     obtain mthd where
   890       "G\<turnstile>mdecl (sig,mthd) declared_in C" 
   891       by (auto simp add: undeclared_in_def declared_in_def
   892                          cdeclaredmethd_def)
   893     with mid show ?thesis 
   894       by auto
   895   qed
   896 qed
   897 
   898 lemma unique_declared_in:
   899  "\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk>
   900  \<Longrightarrow> m = n"
   901 by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
   902             split: memberdecl.splits)
   903 
   904 lemma unique_member_of: 
   905   assumes n: "G\<turnstile>n member_of C" and  
   906           m: "G\<turnstile>m member_of C" and
   907        eqid: "memberid n = memberid m"
   908   shows "n=m"
   909 proof -
   910   from n m eqid  
   911   show "n=m"
   912   proof (induct)
   913     case (Immediate n C)
   914     assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C"
   915     assume eqid: "memberid n = memberid m"
   916     assume "G \<turnstile> m member_of C"
   917     then show "n=m"
   918     proof (cases)
   919       case (Immediate m' _)
   920       with eqid 
   921       have "m=m'"
   922            "memberid n = memberid m" 
   923            "G\<turnstile> mbr m declared_in C" 
   924            "declclass m = C"
   925         by auto
   926       with member_n   
   927       show ?thesis
   928         by (cases n, cases m) 
   929            (auto simp add: declared_in_def 
   930                            cdeclaredmethd_def cdeclaredfield_def
   931                     split: memberdecl.splits)
   932     next
   933       case (Inherited m' _ _)
   934       then have "G\<turnstile> memberid m undeclared_in C"
   935         by simp
   936       with eqid member_n
   937       show ?thesis
   938         by (cases n) (auto dest: declared_not_undeclared)
   939     qed
   940   next
   941     case (Inherited n C S)
   942     assume undecl: "G\<turnstile> memberid n undeclared_in C"
   943     assume  super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S"
   944     assume    hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m"
   945     assume   eqid: "memberid n = memberid m"
   946     assume "G \<turnstile> m member_of C"
   947     then show "n=m"
   948     proof (cases)
   949       case Immediate
   950       then have "G\<turnstile> mbr m declared_in C" by simp
   951       with eqid undecl
   952       show ?thesis
   953         by (cases m) (auto dest: declared_not_undeclared)
   954     next
   955       case Inherited 
   956       with super have "G \<turnstile> m member_of S"
   957         by (auto dest!: subcls1D)
   958       with eqid hyp
   959       show ?thesis 
   960         by blast
   961     qed
   962   qed
   963 qed
   964 
   965 lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C"
   966 proof (induct set: members)
   967   case (Immediate m C)
   968   assume "G\<turnstile> mbr m declared_in C"
   969   then show "is_class G C"
   970     by (cases "mbr m")
   971        (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
   972 next
   973   case (Inherited m C S)  
   974   assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S"
   975   then show "is_class G C"
   976     by - (rule subcls_is_class2,auto)
   977 qed
   978 
   979 lemma member_of_declC: 
   980  "G\<turnstile>m member_of C 
   981   \<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)"
   982 by (induct set: members) auto
   983 
   984 lemma member_of_member_of_declC:
   985  "G\<turnstile>m member_of C 
   986   \<Longrightarrow> G\<turnstile>m member_of (declclass m)"
   987 by (auto dest: member_of_declC intro: members.Immediate)
   988 
   989 lemma member_of_class_relation:
   990   "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
   991 proof (induct set: members)
   992   case (Immediate m C)
   993   then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp
   994 next
   995   case (Inherited m C S)
   996   then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
   997     by (auto dest: r_into_rtrancl intro: rtrancl_trans)
   998 qed
   999 
  1000 lemma member_in_class_relation:
  1001   "G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1002 by (auto dest: member_inD member_of_class_relation
  1003         intro: rtrancl_trans)
  1004 
  1005 lemma stat_override_declclasses_relation: 
  1006 "\<lbrakk>G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; G \<turnstile>Method old member_of superNew \<rbrakk>
  1007 \<Longrightarrow> G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old)"
  1008 apply (rule trancl_rtrancl_trancl)
  1009 apply (erule r_into_trancl)
  1010 apply (cases old)
  1011 apply (auto dest: member_of_class_relation)
  1012 done
  1013 
  1014 lemma stat_overrides_commonD:
  1015 "\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow>  
  1016   declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 
  1017   G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
  1018   G\<turnstile>Method new declared_in (declclass new) \<and>   
  1019   G\<turnstile>Method old declared_in (declclass old)"
  1020 apply (induct set: stat_overridesR) 
  1021 apply (frule (1) stat_override_declclasses_relation) 
  1022 apply (auto intro: trancl_trans)
  1023 done
  1024 
  1025 lemma member_of_Package: 
  1026  "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
  1027   \<Longrightarrow> pid (declclass m) = pid C" 
  1028 proof -
  1029   assume   member: "G\<turnstile>m member_of C"
  1030   then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
  1031   proof (induct rule: members.induct)
  1032     fix C m
  1033     assume     C: "declclass m = C"
  1034     then show "pid (declclass m) = pid C"
  1035       by simp
  1036   next
  1037     fix C S m  
  1038     assume inheritable: "G \<turnstile> m inheritable_in pid C"
  1039     assume         hyp: "PROP ?P m S" and
  1040            package_acc: "accmodi m = Package" 
  1041     with inheritable package_acc hyp
  1042     show "pid (declclass m) = pid C" 
  1043       by (auto simp add: inheritable_in_def)
  1044   qed
  1045 qed
  1046 
  1047 lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
  1048 proof -
  1049   assume member_in_C:  "G\<turnstile>m member_in C"
  1050   from member_in_C
  1051   obtain provC where
  1052     subclseq_C_provC: "G\<turnstile> C \<preceq>\<^sub>C provC" and
  1053      member_of_provC: "G \<turnstile> m member_of provC"
  1054     by (auto simp add: member_in_def)
  1055   from member_of_provC
  1056   have "G \<turnstile> m member_of declclass m"
  1057     by (rule member_of_member_of_declC)
  1058   moreover
  1059   from member_in_C
  1060   have "G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1061     by (rule member_in_class_relation)
  1062   ultimately
  1063   show ?thesis
  1064     by (auto simp add: member_in_def)
  1065 qed
  1066 
  1067 lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S
  1068  \<Longrightarrow> G\<turnstile>m member_in C"
  1069 by (auto elim: dyn_accessible_fromR.induct)
  1070 
  1071 lemma no_Private_stat_override: 
  1072  "\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
  1073 by (induct set:  stat_overridesR) (auto simp add: inheritable_in_def)
  1074 
  1075 lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private"
  1076 by (induct set: overridesR) (auto simp add: inheritable_in_def)
  1077 
  1078 lemma permits_acc_inheritance:
  1079  "\<lbrakk>G\<turnstile>m in statC permits_acc_from accC; G\<turnstile>dynC \<preceq>\<^sub>C statC
  1080   \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_from accC"
  1081 by (cases "accmodi m")
  1082    (auto simp add: permits_acc_def
  1083             intro: subclseq_trans) 
  1084 
  1085 lemma permits_acc_static_declC:
  1086  "\<lbrakk>G\<turnstile>m in C permits_acc_from accC; G\<turnstile>m member_in C; is_static m
  1087   \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_from accC"
  1088 by (cases "accmodi m") (auto simp add: permits_acc_def)
  1089 
  1090 lemma dyn_accessible_from_static_declC: 
  1091   assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
  1092            static: "is_static m"
  1093   shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
  1094 proof -
  1095   from acc_C static
  1096   show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
  1097   proof (induct)
  1098     case (Immediate m C)
  1099     then show ?case 
  1100       by (auto intro!: dyn_accessible_fromR.Immediate
  1101                  dest: member_in_declC permits_acc_static_declC) 
  1102   next 
  1103     case (Overriding m C declCNew new old sup)
  1104     then have "\<not> is_static m"
  1105       by (auto dest: overrides_commonD)
  1106     moreover
  1107     assume "is_static m"
  1108     ultimately show ?case 
  1109       by contradiction
  1110   qed
  1111 qed
  1112 
  1113 lemma field_accessible_fromD:
  1114  "\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 
  1115   \<Longrightarrow> G\<turnstile>membr member_of C \<and>
  1116       G\<turnstile>(Class C) accessible_in (pid accC) \<and>
  1117       G\<turnstile>membr in C permits_acc_from accC"
  1118 by (cases set: accessible_fromR)
  1119    (auto simp add: is_field_def split: memberdecl.splits) 
  1120 
  1121 lemma field_accessible_from_permits_acc_inheritance:
  1122 "\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk>
  1123 \<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC"
  1124 by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
  1125 
  1126 
  1127 (*
  1128 lemma accessible_Package:
  1129  "\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package;
  1130    \<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk>
  1131   \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
  1132 proof -
  1133   assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new"
  1134   assume "G \<turnstile> m of C accessible_from S"
  1135   then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)"
  1136     (is "?Pack m \<Longrightarrow> ?P C m")
  1137   proof (induct rule: accessible_fromR.induct)
  1138     fix C m
  1139     assume "G\<turnstile>m member_of C"
  1140            "G \<turnstile> m in C permits_acc_from S"
  1141            "accmodi m = Package"      
  1142     then show "?P C m"
  1143       by (auto dest: member_of_Package simp add: permits_acc_def)
  1144   next
  1145     fix declC C new newm old Sup
  1146     assume member_new: "G \<turnstile> new member_of C" and 
  1147                 acc_C: "G \<turnstile> Class C accessible_in pid S" and
  1148                   new: "new = (declC, mdecl newm)" and
  1149              override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and
  1150          subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and
  1151               acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and
  1152                   hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and
  1153           accmodi_new: "accmodi new = Package"
  1154     from override wf 
  1155     have accmodi_weaken: "accmodi old \<le> accmodi newm"
  1156       by (cases old,cases newm) auto
  1157     from override new
  1158     have "accmodi old \<noteq> Private"
  1159       by (simp add: no_Private_stat_override)
  1160     with accmodi_weaken accmodi_new new
  1161     have accmodi_old: "accmodi old = Package"
  1162       by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 
  1163     with hyp 
  1164     have P_sup: "?P Sup (methdMembr old)"
  1165       by (simp)
  1166     from wf override new accmodi_old accmodi_new
  1167     have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
  1168       by (auto dest: stat_override_Package) 
  1169     from member_new accmodi_new
  1170     have "pid (declclass new) = pid C"
  1171       by (auto dest: member_of_Package)
  1172     with eq_pid_new_old P_sup show "?P C new"
  1173       by auto
  1174   qed
  1175 qed
  1176 *)
  1177 
  1178 lemma accessible_fieldD: 
  1179  "\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk>
  1180  \<Longrightarrow> G\<turnstile>membr member_of C \<and>
  1181      G\<turnstile>(Class C) accessible_in (pid accC) \<and>
  1182      G\<turnstile>membr in C permits_acc_from accC"
  1183 by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
  1184       
  1185 
  1186 
  1187 lemma member_of_Private:
  1188 "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C"
  1189 by (induct set: members) (auto simp add: inheritable_in_def)
  1190 
  1191 lemma member_of_subclseq_declC:
  1192   "G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m"
  1193 by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
  1194 
  1195 lemma member_of_inheritance:
  1196   assumes       m: "G\<turnstile>m member_of D" and
  1197      subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
  1198      subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
  1199                ws: "ws_prog G" 
  1200   shows "G\<turnstile>m member_of C"
  1201 proof -
  1202   from m subclseq_D_C subclseq_C_m
  1203   show ?thesis
  1204   proof (induct)
  1205     case (Immediate m D)
  1206     assume "declclass m = D" and
  1207            "G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m"
  1208     with ws have "D=C" 
  1209       by (auto intro: subclseq_acyclic)
  1210     with Immediate 
  1211     show "G\<turnstile>m member_of C"
  1212       by (auto intro: members.Immediate)
  1213   next
  1214     case (Inherited m D S)
  1215     assume member_of_D_props: 
  1216             "G \<turnstile> m inheritable_in pid D" 
  1217             "G\<turnstile> memberid m undeclared_in D"  
  1218             "G \<turnstile> Class S accessible_in pid D" 
  1219             "G \<turnstile> m member_of S"
  1220     assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S"
  1221     assume hyp: "\<lbrakk>G\<turnstile>S\<preceq>\<^sub>C C; G\<turnstile>C\<preceq>\<^sub>C declclass m\<rbrakk> \<Longrightarrow> G \<turnstile> m member_of C"
  1222     assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m"
  1223     assume "G\<turnstile>D\<preceq>\<^sub>C C"
  1224     then show "G\<turnstile>m member_of C"
  1225     proof (cases rule: subclseq_cases)
  1226       case Eq
  1227       assume "D=C" 
  1228       with super member_of_D_props 
  1229       show ?thesis
  1230         by (auto intro: members.Inherited)
  1231     next
  1232       case Subcls
  1233       assume "G\<turnstile>D\<prec>\<^sub>C C"
  1234       with super 
  1235       have "G\<turnstile>S\<preceq>\<^sub>C C"
  1236         by (auto dest: subcls1D subcls_superD)
  1237       with subclseq_C_m hyp show ?thesis
  1238         by blast
  1239     qed
  1240   qed
  1241 qed
  1242 
  1243 lemma member_of_subcls:
  1244   assumes     old: "G\<turnstile>old member_of C" and 
  1245               new: "G\<turnstile>new member_of D" and
  1246              eqid: "memberid new = memberid old" and
  1247      subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
  1248    subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
  1249                ws: "ws_prog G"
  1250   shows "G\<turnstile>D \<prec>\<^sub>C C"
  1251 proof -
  1252   from old 
  1253   have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
  1254     by (auto dest: member_of_subclseq_declC)
  1255   from new 
  1256   have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new"
  1257     by (auto dest: member_of_subclseq_declC)
  1258   from subcls_new_old ws
  1259   have neq_new_old: "new\<noteq>old"
  1260     by (cases new,cases old) (auto dest: subcls_irrefl)
  1261   from subclseq_D_new subclseq_D_C
  1262   have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 
  1263     by (rule subcls_compareable)
  1264   then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C"
  1265   proof
  1266     assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis .
  1267   next
  1268     assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)"
  1269     with new subclseq_D_C ws 
  1270     have "G\<turnstile>new member_of C"
  1271       by (blast intro: member_of_inheritance)
  1272     with eqid old 
  1273     have "new=old"
  1274       by (blast intro: unique_member_of)
  1275     with neq_new_old 
  1276     show ?thesis
  1277       by contradiction
  1278   qed
  1279   then show ?thesis
  1280   proof (cases rule: subclseq_cases)
  1281     case Eq
  1282     assume "declclass new = C"
  1283     with new have "G\<turnstile>new member_of C"
  1284       by (auto dest: member_of_member_of_declC)
  1285     with eqid old 
  1286     have "new=old"
  1287       by (blast intro: unique_member_of)
  1288     with neq_new_old 
  1289     show ?thesis
  1290       by contradiction
  1291   next
  1292     case Subcls
  1293     assume "G\<turnstile>declclass new\<prec>\<^sub>C C"
  1294     with subclseq_D_new
  1295     show "G\<turnstile>D\<prec>\<^sub>C C"
  1296       by (rule rtrancl_trancl_trancl)
  1297   qed
  1298 qed
  1299 
  1300 corollary member_of_overrides_subcls:
  1301  "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
  1302    G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk>
  1303  \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
  1304 by (drule overrides_commonD) (auto intro: member_of_subcls)    
  1305 
  1306 corollary member_of_stat_overrides_subcls:
  1307  "\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C;
  1308    G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk>
  1309  \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C"
  1310 by (drule stat_overrides_commonD) (auto intro: member_of_subcls)    
  1311 
  1312 
  1313 
  1314 lemma inherited_field_access: 
  1315   assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
  1316           is_field: "is_field membr" and 
  1317           subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
  1318   shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
  1319 proof -
  1320   from stat_acc is_field subclseq 
  1321   show ?thesis
  1322     by (auto dest: accessible_fieldD 
  1323             intro: dyn_accessible_fromR.Immediate 
  1324                    member_inI 
  1325                    permits_acc_inheritance)
  1326 qed
  1327 
  1328 lemma accessible_inheritance:
  1329   assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
  1330           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  1331        member_dynC: "G\<turnstile>m member_of dynC" and
  1332           dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
  1333   shows "G\<turnstile>m of dynC accessible_from accC"
  1334 proof -
  1335   from stat_acc
  1336   have member_statC: "G\<turnstile>m member_of statC" 
  1337     by (auto dest: accessible_from_commonD)
  1338   from stat_acc
  1339   show ?thesis
  1340   proof (cases)
  1341     case Immediate
  1342     with member_dynC member_statC subclseq dynC_acc
  1343     show ?thesis
  1344       by (auto intro: accessible_fromR.Immediate permits_acc_inheritance)
  1345   next
  1346     case Overriding
  1347     with member_dynC subclseq dynC_acc
  1348     show ?thesis
  1349       by (auto intro: accessible_fromR.Overriding rtrancl_trancl_trancl)
  1350   qed
  1351 qed
  1352 
  1353 section "fields and methods"
  1354 
  1355 
  1356 types
  1357   fspec = "vname \<times> qtname"
  1358 
  1359 translations 
  1360   "fspec" <= (type) "vname \<times> qtname" 
  1361 
  1362 constdefs
  1363 imethds:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
  1364 "imethds G I 
  1365   \<equiv> iface_rec (G,I)  
  1366               (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
  1367                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
  1368 text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
  1369 
  1370 constdefs
  1371 accimethds:: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables"
  1372 "accimethds G pack I
  1373   \<equiv> if G\<turnstile>Iface I accessible_in pack 
  1374        then imethds G I
  1375        else \<lambda> k. {}"
  1376 text {* only returns imethds if the interface is accessible *}
  1377 
  1378 constdefs
  1379 methd:: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
  1380 
  1381 "methd G C 
  1382  \<equiv> class_rec (G,C) empty
  1383              (\<lambda>C c subcls_mthds. 
  1384                filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
  1385                           subcls_mthds 
  1386                ++ 
  1387                table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))"
  1388 text {* @{term "methd G C"}: methods of a class C (statically visible from C), 
  1389      with inheritance and hiding cf. 8.4.6;
  1390      Overriding is captured by @{text dynmethd}.
  1391      Every new method with the same signature coalesces the
  1392      method of a superclass. *}
  1393 
  1394 constdefs                      
  1395 accmethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table"
  1396 "accmethd G S C 
  1397  \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) 
  1398               (methd G C)"
  1399 text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"}, 
  1400         accessible from S *}
  1401 
  1402 text {* Note the class component in the accessibility filter. The class where
  1403     method @{term m} is declared (@{term declC}) isn't necessarily accessible 
  1404     from the current scope @{term S}. The method can be made accessible 
  1405     through inheritance, too.
  1406     So we must test accessibility of method @{term m} of class @{term C} 
  1407     (not @{term "declclass m"}) *}
  1408 
  1409 constdefs 
  1410 dynmethd:: "prog  \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
  1411 "dynmethd G statC dynC  
  1412   \<equiv> \<lambda> sig. 
  1413      (if G\<turnstile>dynC \<preceq>\<^sub>C statC
  1414         then (case methd G statC sig of
  1415                 None \<Rightarrow> None
  1416               | Some statM 
  1417                   \<Rightarrow> (class_rec (G,dynC) empty
  1418                        (\<lambda>C c subcls_mthds. 
  1419                           subcls_mthds
  1420                           ++
  1421                           (filter_tab 
  1422                             (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
  1423                             (methd G C) ))
  1424                       ) sig
  1425               )
  1426         else None)"
  1427 
  1428 text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference 
  1429         with dynamic class @{term dynC} and static class @{term statC} *}
  1430 text {* Note some kind of duality between @{term methd} and @{term dynmethd} 
  1431         in the @{term class_rec} arguments. Whereas @{term methd} filters the 
  1432         subclass methods (to get only the inherited ones), @{term dynmethd} 
  1433         filters the new methods (to get only those methods which actually
  1434         override the methods of the static class) *}
  1435 
  1436 constdefs 
  1437 dynimethd:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
  1438 "dynimethd G I dynC 
  1439   \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
  1440                then methd G dynC sig
  1441                else dynmethd G Object dynC sig"
  1442 text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with 
  1443         dynamic class dynC and static interface type I *}
  1444 text {* 
  1445    When calling an interface method, we must distinguish if the method signature
  1446    was defined in the interface or if it must be an Object method in the other
  1447    case. If it was an interface method we search the class hierarchy
  1448    starting at the dynamic class of the object up to Object to find the 
  1449    first matching method (@{term methd}). Since all interface methods have 
  1450    public access the method can't be coalesced due to some odd visibility 
  1451    effects like in case of dynmethd. The method will be inherited or 
  1452    overridden in all classes from the first class implementing the interface 
  1453    down to the actual dynamic class.
  1454  *}
  1455 
  1456 constdefs
  1457 dynlookup::"prog  \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table"
  1458 "dynlookup G statT dynC
  1459   \<equiv> (case statT of
  1460        NullT        \<Rightarrow> empty
  1461      | IfaceT I     \<Rightarrow> dynimethd G I      dynC
  1462      | ClassT statC \<Rightarrow> dynmethd  G statC  dynC
  1463      | ArrayT ty    \<Rightarrow> dynmethd  G Object dynC)"
  1464 text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the 
  1465     static reference type statT and the dynamic class dynC. 
  1466     In a wellformd context statT will not be NullT and in case
  1467     statT is an array type, dynC=Object *}
  1468 
  1469 constdefs
  1470 fields:: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list"
  1471 "fields G C 
  1472   \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
  1473 text {* @{term "fields G C"} 
  1474      list of fields of a class, including all the fields of the superclasses
  1475      (private, inherited and hidden ones) not only the accessible ones
  1476      (an instance of a object allocates all these fields *}
  1477 
  1478 constdefs
  1479 accfield:: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname  \<times>  field) table"
  1480 "accfield G S C
  1481   \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
  1482     in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
  1483                   field_tab"
  1484 text  {* @{term "accfield G C S"}: fields of a class @{term C} which are 
  1485          accessible from scope of class
  1486          @{term S} with inheritance and hiding, cf. 8.3 *}
  1487 text {* note the class component in the accessibility filter (see also 
  1488         @{term methd}).
  1489    The class declaring field @{term f} (@{term declC}) isn't necessarily 
  1490    accessible from scope @{term S}. The field can be made visible through 
  1491    inheritance, too. So we must test accessibility of field @{term f} of class 
  1492    @{term C} (not @{term "declclass f"}) *} 
  1493 
  1494 constdefs
  1495 
  1496   is_methd :: "prog \<Rightarrow> qtname  \<Rightarrow> sig \<Rightarrow> bool"
  1497  "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
  1498 
  1499 constdefs efname:: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
  1500 "efname \<equiv> fst"
  1501 
  1502 lemma efname_simp[simp]:"efname (n,f) = n"
  1503 by (simp add: efname_def) 
  1504 
  1505 
  1506 subsection "imethds"
  1507 
  1508 lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
  1509   imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
  1510                       (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
  1511 apply (unfold imethds_def)
  1512 apply (rule iface_rec [THEN trans])
  1513 apply auto
  1514 done
  1515 
  1516 
  1517 (* local lemma *)
  1518 lemma imethds_norec:
  1519   "\<lbrakk>iface G md = Some i; ws_prog G; table_of (imethods i) sig = Some mh\<rbrakk> \<Longrightarrow>  
  1520   (md, mh) \<in> imethds G md sig"
  1521 apply (subst imethds_rec)
  1522 apply assumption+
  1523 apply (rule iffD2)
  1524 apply (rule overrides_t_Some_iff)
  1525 apply (rule disjI1)
  1526 apply (auto elim: table_of_map_SomeI)
  1527 done
  1528 
  1529 lemma imethds_declI: "\<lbrakk>m \<in> imethds G I sig; ws_prog G; is_iface G I\<rbrakk> \<Longrightarrow> 
  1530   (\<exists>i. iface G (decliface m) = Some i \<and> 
  1531   table_of (imethods i) sig = Some (mthd m)) \<and>  
  1532   (I,decliface m) \<in> (subint1 G)^* \<and> m \<in> imethds G (decliface m) sig"
  1533 apply (erule rev_mp)
  1534 apply (rule ws_subint1_induct, assumption, assumption)
  1535 apply (subst imethds_rec, erule conjunct1, assumption)
  1536 apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
  1537 done
  1538 
  1539 lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
  1540   assumes im: "im \<in> imethds G I sig" and  
  1541          ifI: "iface G I = Some i" and
  1542           ws: "ws_prog G" and
  1543      hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
  1544                 = Some im \<Longrightarrow> P" and
  1545      hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
  1546   shows P
  1547 proof -
  1548   from ifI ws im hyp_new hyp_inh
  1549   show "P"
  1550     by (auto simp add: imethds_rec)
  1551 qed
  1552 
  1553 subsection "accimethd"
  1554 
  1555 lemma accimethds_simp [simp]: 
  1556 "G\<turnstile>Iface I accessible_in pack \<Longrightarrow> accimethds G pack I = imethds G I"
  1557 by (simp add: accimethds_def)
  1558 
  1559 lemma accimethdsD:
  1560  "im \<in> accimethds G pack I sig 
  1561   \<Longrightarrow> im \<in> imethds G I sig \<and> G\<turnstile>Iface I accessible_in pack"
  1562 by (auto simp add: accimethds_def)
  1563 
  1564 lemma accimethdsI: 
  1565 "\<lbrakk>im \<in> imethds G I sig;G\<turnstile>Iface I accessible_in pack\<rbrakk>
  1566  \<Longrightarrow> im \<in> accimethds G pack I sig"
  1567 by simp
  1568 
  1569 subsection "methd"
  1570 
  1571 lemma methd_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
  1572   methd G C 
  1573     = (if C = Object 
  1574           then empty 
  1575           else filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
  1576                           (methd G (super c))) 
  1577       ++ table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))"
  1578 apply (unfold methd_def)
  1579 apply (erule class_rec [THEN trans], assumption)
  1580 apply (simp)
  1581 done
  1582 
  1583 (* local lemma *)
  1584 lemma methd_norec: 
  1585  "\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> 
  1586   \<Longrightarrow> methd G declC sig = Some (declC, m)"
  1587 apply (simp only: methd_rec)
  1588 apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
  1589 apply (auto elim: table_of_map_SomeI)
  1590 done
  1591 
  1592 
  1593 lemma methd_declC: 
  1594 "\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> \<Longrightarrow>
  1595  (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and> 
  1596  G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"   
  1597 apply (erule rev_mp)
  1598 apply (rule ws_subcls1_induct, assumption, assumption)
  1599 apply (subst methd_rec, assumption)
  1600 apply (case_tac "Ca=Object")
  1601 apply   (force elim: methd_norec )
  1602 
  1603 apply   simp
  1604 apply   (case_tac "table_of (map (\<lambda>(s, m). (s, Ca, m)) (methods c)) sig")
  1605 apply     (force intro: rtrancl_into_rtrancl2)
  1606 
  1607 apply     (auto intro: methd_norec)
  1608 done
  1609 
  1610 lemma methd_inheritedD:
  1611   "\<lbrakk>class G C = Some c; ws_prog G;methd G C sig = Some m\<rbrakk>
  1612   \<Longrightarrow>  (declclass m \<noteq> C \<longrightarrow> G \<turnstile>C inherits method sig m)"
  1613 by (auto simp add: methd_rec)
  1614 
  1615 lemma methd_diff_cls:
  1616 "\<lbrakk>ws_prog G; is_class G C; is_class G D;
  1617  methd G C sig = m; methd G D sig = n; m\<noteq>n
  1618 \<rbrakk> \<Longrightarrow> C\<noteq>D"
  1619 by (auto simp add: methd_rec)
  1620 
  1621 lemma method_declared_inI: 
  1622  "\<lbrakk>table_of (methods c) sig = Some m; class G C = Some c\<rbrakk>
  1623   \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
  1624 by (auto simp add: cdeclaredmethd_def declared_in_def)
  1625 
  1626 lemma methd_declared_in_declclass: 
  1627  "\<lbrakk>methd G C sig = Some m; ws_prog G;is_class G C\<rbrakk> 
  1628  \<Longrightarrow> G\<turnstile>Methd sig m declared_in (declclass m)"
  1629 by (auto dest: methd_declC method_declared_inI)
  1630 
  1631 lemma member_methd:
  1632   assumes member_of: "G\<turnstile>Methd sig m member_of C" and
  1633                  ws: "ws_prog G"
  1634   shows "methd G C sig = Some m"
  1635 proof -
  1636   from member_of 
  1637   have iscls_C: "is_class G C" 
  1638     by (rule member_of_is_classD)
  1639   from iscls_C ws member_of
  1640   show ?thesis (is "?Methd C")
  1641   proof (induct rule: ws_class_induct')
  1642     case (Object co)
  1643     assume "G \<turnstile>Methd sig m member_of Object"
  1644     then have "G\<turnstile>Methd sig m declared_in Object \<and> declclass m = Object"
  1645       by (cases set: members) (cases m, auto dest: subcls1D)
  1646     with ws Object 
  1647     show "?Methd Object"
  1648       by (cases m)
  1649          (auto simp add: declared_in_def cdeclaredmethd_def methd_rec
  1650                   intro:  table_of_mapconst_SomeI)
  1651   next
  1652     case (Subcls C c)
  1653     assume clsC: "class G C = Some c" and
  1654       neq_C_Obj: "C \<noteq> Object" and
  1655             hyp: "G \<turnstile>Methd sig m member_of super c \<Longrightarrow> ?Methd (super c)" and
  1656       member_of: "G \<turnstile>Methd sig m member_of C"
  1657     from member_of
  1658     show "?Methd C"
  1659     proof (cases)
  1660       case (Immediate membr Ca)
  1661       then have "Ca=C" "membr = method sig m" and 
  1662                 "G\<turnstile>Methd sig m declared_in C" "declclass m = C"
  1663         by (cases m,auto)
  1664       with clsC 
  1665       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m"
  1666         by (cases m)
  1667            (auto simp add: declared_in_def cdeclaredmethd_def
  1668                     intro: table_of_mapconst_SomeI)
  1669       with clsC neq_C_Obj ws 
  1670       show ?thesis
  1671         by (simp add: methd_rec)
  1672     next
  1673       case (Inherited membr Ca S)
  1674       with clsC
  1675       have eq_Ca_C: "Ca=C" and
  1676             undecl: "G\<turnstile>mid sig undeclared_in C" and
  1677              super: "G \<turnstile>Methd sig m member_of (super c)"
  1678         by (auto dest: subcls1D)
  1679       from eq_Ca_C clsC undecl 
  1680       have "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = None"
  1681         by (auto simp add: undeclared_in_def cdeclaredmethd_def
  1682                     intro: table_of_mapconst_NoneI)
  1683       moreover
  1684       from Inherited have "G \<turnstile> C inherits (method sig m)"
  1685         by (auto simp add: inherits_def)
  1686       moreover
  1687       note clsC neq_C_Obj ws super hyp 
  1688       ultimately
  1689       show ?thesis
  1690         by (auto simp add: methd_rec intro: filter_tab_SomeI)
  1691     qed
  1692   qed
  1693 qed
  1694 
  1695 (*unused*)
  1696 lemma finite_methd:"ws_prog G \<Longrightarrow> finite {methd G C sig |sig C. is_class G C}"
  1697 apply (rule finite_is_class [THEN finite_SetCompr2])
  1698 apply (intro strip)
  1699 apply (erule_tac ws_subcls1_induct, assumption)
  1700 apply (subst methd_rec)
  1701 apply (assumption)
  1702 apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
  1703 done
  1704 
  1705 lemma finite_dom_methd:
  1706  "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (methd G C))"
  1707 apply (erule_tac ws_subcls1_induct)
  1708 apply assumption
  1709 apply (subst methd_rec)
  1710 apply (assumption)
  1711 apply (auto intro!: finite_dom_map_of finite_dom_filter_tab)
  1712 done
  1713 
  1714 
  1715 subsection "accmethd"
  1716 
  1717 lemma accmethd_SomeD:
  1718 "accmethd G S C sig = Some m
  1719  \<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S"
  1720 by (auto simp add: accmethd_def dest: filter_tab_SomeD)
  1721 
  1722 lemma accmethd_SomeI:
  1723 "\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk> 
  1724  \<Longrightarrow> accmethd G S C sig = Some m"
  1725 by (auto simp add: accmethd_def intro: filter_tab_SomeI)
  1726 
  1727 lemma accmethd_declC: 
  1728 "\<lbrakk>accmethd G S C sig = Some m; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>
  1729  (\<exists>d. class G (declclass m)=Some d \<and> 
  1730   table_of (methods d) sig=Some (mthd m)) \<and> 
  1731  G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m \<and> 
  1732  G\<turnstile>method sig m of C accessible_from S"
  1733 by (auto dest: accmethd_SomeD methd_declC accmethd_SomeI)
  1734 
  1735 
  1736 lemma finite_dom_accmethd:
  1737  "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (accmethd G S C))"
  1738 by (auto simp add: accmethd_def intro: finite_dom_filter_tab finite_dom_methd)
  1739 
  1740 
  1741 subsection "dynmethd"
  1742 
  1743 lemma dynmethd_rec:
  1744 "\<lbrakk>class G dynC = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
  1745  dynmethd G statC dynC sig
  1746    = (if G\<turnstile>dynC \<preceq>\<^sub>C statC
  1747         then (case methd G statC sig of
  1748                 None \<Rightarrow> None
  1749               | Some statM 
  1750                   \<Rightarrow> (case methd G dynC sig of
  1751                         None \<Rightarrow> dynmethd G statC (super c) sig
  1752                       | Some dynM \<Rightarrow> 
  1753                           (if G,sig\<turnstile> dynM overrides statM \<or> dynM = statM 
  1754                               then Some dynM
  1755                               else (dynmethd G statC (super c) sig)
  1756                       )))
  1757          else None)" 
  1758    (is "_ \<Longrightarrow> _ \<Longrightarrow> ?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig") 
  1759 proof -
  1760   assume clsDynC: "class G dynC = Some c" and 
  1761               ws: "ws_prog G"
  1762   then show "?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig" 
  1763   proof (induct rule: ws_class_induct'')
  1764     case (Object co)
  1765     show "?Dynmethd_def Object sig = ?Dynmethd_rec Object co sig"
  1766     proof (cases "G\<turnstile>Object \<preceq>\<^sub>C statC") 
  1767       case False
  1768       then show ?thesis by (simp add: dynmethd_def)
  1769     next
  1770       case True
  1771       then have eq_statC_Obj: "statC = Object" ..
  1772       show ?thesis 
  1773       proof (cases "methd G statC sig")
  1774         case None then show ?thesis by (simp add: dynmethd_def)
  1775       next
  1776         case Some
  1777         with True Object ws eq_statC_Obj 
  1778         show ?thesis
  1779           by (auto simp add: dynmethd_def class_rec
  1780                       intro: filter_tab_SomeI)
  1781       qed
  1782     qed
  1783   next  
  1784     case (Subcls dynC c sc)
  1785     show "?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig"
  1786     proof (cases "G\<turnstile>dynC \<preceq>\<^sub>C statC") 
  1787       case False
  1788       then show ?thesis by (simp add: dynmethd_def)
  1789     next
  1790       case True
  1791       note subclseq_dynC_statC = True
  1792       show ?thesis
  1793       proof (cases "methd G statC sig")
  1794         case None then show ?thesis by (simp add: dynmethd_def)
  1795       next
  1796         case (Some statM)
  1797         note statM = Some
  1798         let "?filter C" = 
  1799               "filter_tab
  1800                 (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
  1801                 (methd G C)"
  1802         let "?class_rec C" =
  1803               "(class_rec (G, C) empty
  1804                            (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
  1805         from statM Subcls ws subclseq_dynC_statC
  1806         have dynmethd_dynC_def:
  1807              "?Dynmethd_def dynC sig =
  1808                 ((?class_rec (super c)) 
  1809                  ++
  1810                 (?filter dynC)) sig"
  1811          by (simp (no_asm_simp) only: dynmethd_def class_rec)
  1812             auto
  1813        show ?thesis
  1814        proof (cases "dynC = statC")
  1815          case True
  1816          with subclseq_dynC_statC statM dynmethd_dynC_def
  1817          have "?Dynmethd_def dynC sig = Some statM"
  1818            by (auto intro: map_add_find_right filter_tab_SomeI)
  1819          with subclseq_dynC_statC True Some 
  1820          show ?thesis
  1821            by auto
  1822        next
  1823          case False
  1824          with subclseq_dynC_statC Subcls 
  1825          have subclseq_super_statC: "G\<turnstile>(super c) \<preceq>\<^sub>C statC"
  1826            by (blast dest: subclseq_superD)
  1827          show ?thesis
  1828          proof (cases "methd G dynC sig") 
  1829            case None
  1830            then have "?filter dynC sig = None"
  1831              by (rule filter_tab_None)
  1832            then have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
  1833              by (simp add: dynmethd_dynC_def)
  1834            with  subclseq_super_statC statM None
  1835            have "?Dynmethd_def dynC sig = ?Dynmethd_def (super c) sig"
  1836              by (auto simp add: empty_def dynmethd_def)
  1837            with None subclseq_dynC_statC statM
  1838            show ?thesis 
  1839              by simp
  1840          next
  1841            case (Some dynM)
  1842            note dynM = Some
  1843            let ?Termination = "G \<turnstile> qmdecl sig dynM overrides qmdecl sig statM \<or>
  1844                                dynM = statM"
  1845            show ?thesis
  1846            proof (cases "?filter dynC sig")
  1847              case None
  1848              with dynM 
  1849              have no_termination: "\<not> ?Termination"
  1850                by (simp add: filter_tab_def)
  1851              from None 
  1852              have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
  1853                by (simp add: dynmethd_dynC_def)
  1854              with subclseq_super_statC statM dynM no_termination
  1855              show ?thesis
  1856                by (auto simp add: empty_def dynmethd_def)
  1857            next
  1858              case Some
  1859              with dynM
  1860              have "termination": "?Termination"
  1861                by (auto)
  1862              with Some dynM
  1863              have "?Dynmethd_def dynC sig=Some dynM"
  1864               by (auto simp add: dynmethd_dynC_def)
  1865              with subclseq_super_statC statM dynM "termination"
  1866              show ?thesis
  1867                by (auto simp add: dynmethd_def)
  1868            qed
  1869          qed
  1870        qed
  1871      qed
  1872    qed
  1873  qed
  1874 qed
  1875                
  1876 lemma dynmethd_C_C:"\<lbrakk>is_class G C; ws_prog G\<rbrakk> 
  1877 \<Longrightarrow> dynmethd G C C sig = methd G C sig"          
  1878 apply (auto simp add: dynmethd_rec)
  1879 done
  1880  
  1881 lemma dynmethdSomeD: 
  1882  "\<lbrakk>dynmethd G statC dynC sig = Some dynM; is_class G dynC; ws_prog G\<rbrakk> 
  1883   \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
  1884 by (auto simp add: dynmethd_rec)
  1885  
  1886 lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
  1887   assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
  1888         is_cls_dynC: "is_class G dynC" and
  1889                  ws: "ws_prog G" and
  1890          hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
  1891        hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
  1892                        G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
  1893   shows P
  1894 proof -
  1895   from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
  1896   from clsDynC ws dynM hyp_static hyp_override
  1897   show "P"
  1898   proof (induct rule: ws_class_induct)
  1899     case (Object co)
  1900     with ws  have "statC = Object" 
  1901       by (auto simp add: dynmethd_rec)
  1902     with ws Object show ?thesis by (auto simp add: dynmethd_C_C)
  1903   next
  1904     case (Subcls C c)
  1905     with ws show ?thesis
  1906       by (auto simp add: dynmethd_rec)
  1907   qed
  1908 qed
  1909 
  1910 lemma no_override_in_Object:
  1911   assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
  1912             is_cls_dynC: "is_class G dynC" and
  1913                      ws: "ws_prog G" and
  1914                   statM: "methd G statC sig = Some statM" and
  1915          neq_dynM_statM: "dynM\<noteq>statM"
  1916   shows "dynC \<noteq> Object"
  1917 proof -
  1918   from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
  1919   from clsDynC ws dynM statM neq_dynM_statM 
  1920   show ?thesis (is "?P dynC")
  1921   proof (induct rule: ws_class_induct)
  1922     case (Object co)
  1923     with ws  have "statC = Object" 
  1924       by (auto simp add: dynmethd_rec)
  1925     with ws Object show "?P Object" by (auto simp add: dynmethd_C_C)
  1926   next
  1927     case (Subcls dynC c)
  1928     with ws show "?P dynC"
  1929       by (auto simp add: dynmethd_rec)
  1930   qed
  1931 qed
  1932 
  1933 
  1934 lemma dynmethd_Some_rec_cases [consumes 3, 
  1935                                case_names Static Override  Recursion]:
  1936   assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
  1937                 clsDynC: "class G dynC = Some c" and
  1938                      ws: "ws_prog G" and
  1939              hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
  1940            hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;
  1941                                      methd G dynC sig = Some dynM; statM\<noteq>dynM;
  1942                                      G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
  1943 
  1944           hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
  1945                            dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
  1946   shows P
  1947 proof -
  1948   from clsDynC have "is_class G dynC" by simp
  1949   note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
  1950   from ws clsDynC dynM hyp_static hyp_override hyp_recursion
  1951   show ?thesis
  1952     by (auto simp add: dynmethd_rec dest: no_override_in_Object')
  1953 qed
  1954 
  1955 lemma dynmethd_declC: 
  1956 "\<lbrakk>dynmethd G statC dynC sig = Some m;
  1957   is_class G statC;ws_prog G
  1958  \<rbrakk> \<Longrightarrow>
  1959   (\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and>
  1960   G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m"
  1961 proof - 
  1962   assume  is_cls_statC: "is_class G statC" 
  1963   assume            ws: "ws_prog G"  
  1964   assume             m: "dynmethd G statC dynC sig = Some m"
  1965   from m 
  1966   have "G\<turnstile>dynC \<preceq>\<^sub>C statC" by (auto simp add: dynmethd_def)
  1967   from this is_cls_statC 
  1968   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  1969   from is_cls_dynC ws m  
  1970   show ?thesis (is "?P dynC") 
  1971   proof (induct rule: ws_class_induct')
  1972     case (Object co)
  1973     with ws have "statC=Object" by (auto simp add: dynmethd_rec)
  1974     with ws Object  
  1975     show "?P Object" 
  1976       by (auto simp add: dynmethd_C_C dest: methd_declC)
  1977   next
  1978     case (Subcls dynC c)
  1979     assume   hyp: "dynmethd G statC (super c) sig = Some m \<Longrightarrow> ?P (super c)" and
  1980          clsDynC: "class G dynC = Some c"  and
  1981               m': "dynmethd G statC dynC sig = Some m" and
  1982     neq_dynC_Obj: "dynC \<noteq> Object"
  1983     from ws this obtain statM where
  1984       subclseq_dynC_statC: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and 
  1985                      statM: "methd G statC sig = Some statM"
  1986       by (blast dest: dynmethdSomeD)
  1987     from clsDynC neq_dynC_Obj 
  1988     have subclseq_dynC_super: "G\<turnstile>dynC \<preceq>\<^sub>C (super c)" 
  1989       by (auto intro: subcls1I) 
  1990     from m' clsDynC ws 
  1991     show "?P dynC"
  1992     proof (cases rule: dynmethd_Some_rec_cases) 
  1993       case Static
  1994       with is_cls_statC ws subclseq_dynC_statC 
  1995       show ?thesis 
  1996         by (auto intro: rtrancl_trans dest: methd_declC)
  1997     next
  1998       case Override
  1999       with clsDynC ws 
  2000       show ?thesis 
  2001         by (auto dest: methd_declC)
  2002     next
  2003       case Recursion
  2004       with hyp subclseq_dynC_super 
  2005       show ?thesis 
  2006         by (auto intro: rtrancl_trans) 
  2007     qed
  2008   qed
  2009 qed
  2010 
  2011 lemma methd_Some_dynmethd_Some:
  2012   assumes     statM: "methd G statC sig = Some statM" and
  2013            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2014        is_cls_statC: "is_class G statC" and
  2015                  ws: "ws_prog G"
  2016   shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
  2017     (is "?P dynC")
  2018 proof -
  2019   from subclseq is_cls_statC 
  2020   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  2021   then obtain dc where
  2022     clsDynC: "class G dynC = Some dc" by blast
  2023   from clsDynC ws subclseq 
  2024   show "?thesis"
  2025   proof (induct rule: ws_class_induct)
  2026     case (Object co)
  2027     with ws  have "statC = Object" 
  2028       by (auto)
  2029     with ws Object statM
  2030     show "?P Object"  
  2031       by (auto simp add: dynmethd_C_C)
  2032   next
  2033     case (Subcls dynC dc)
  2034     assume clsDynC': "class G dynC = Some dc"
  2035     assume neq_dynC_Obj: "dynC \<noteq> Object"
  2036     assume hyp: "G\<turnstile>super dc\<preceq>\<^sub>C statC \<Longrightarrow> ?P (super dc)"
  2037     assume subclseq': "G\<turnstile>dynC\<preceq>\<^sub>C statC"
  2038     then
  2039     show "?P dynC"
  2040     proof (cases rule: subclseq_cases)
  2041       case Eq
  2042       with ws statM clsDynC' 
  2043       show ?thesis
  2044         by (auto simp add: dynmethd_rec)
  2045     next
  2046       case Subcls
  2047       assume "G\<turnstile>dynC\<prec>\<^sub>C statC"
  2048       from this clsDynC' 
  2049       have "G\<turnstile>super dc\<preceq>\<^sub>C statC" by (rule subcls_superD)
  2050       with hyp ws clsDynC' subclseq' statM
  2051       show ?thesis
  2052         by (auto simp add: dynmethd_rec)
  2053     qed
  2054   qed
  2055 qed
  2056 
  2057 lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
  2058   assumes     statM: "methd G statC sig = Some statM" and 
  2059            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2060        is_cls_statC: "is_class G statC" and
  2061                  ws: "ws_prog G" and
  2062          hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and
  2063        hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
  2064                                  dynM\<noteq>statM;
  2065                            G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
  2066   shows P
  2067 proof -
  2068   from subclseq is_cls_statC 
  2069   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  2070   then obtain dc where
  2071     clsDynC: "class G dynC = Some dc" by blast
  2072   from statM subclseq is_cls_statC ws 
  2073   obtain dynM
  2074     where dynM: "dynmethd G statC dynC sig = Some dynM"
  2075     by (blast dest: methd_Some_dynmethd_Some)
  2076   from dynM is_cls_dynC ws 
  2077   show ?thesis
  2078   proof (cases rule: dynmethd_Some_cases)
  2079     case Static
  2080     with hyp_static dynM statM show ?thesis by simp
  2081   next
  2082     case Overrides
  2083     with hyp_override dynM statM show ?thesis by simp
  2084   qed
  2085 qed
  2086 
  2087 lemma ws_dynmethd:
  2088   assumes  statM: "methd G statC sig = Some statM" and
  2089         subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
  2090     is_cls_statC: "is_class G statC" and
  2091               ws: "ws_prog G"
  2092   shows
  2093     "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
  2094              is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
  2095 proof - 
  2096   from statM subclseq is_cls_statC ws
  2097   show ?thesis
  2098   proof (cases rule: dynmethd_cases)
  2099     case Static
  2100     with statM 
  2101     show ?thesis
  2102       by simp
  2103   next
  2104     case Overrides
  2105     with ws
  2106     show ?thesis
  2107       by (auto dest: ws_overrides_commonD)
  2108   qed
  2109 qed
  2110 
  2111 subsection "dynlookup"
  2112 
  2113 lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]:
  2114 "\<lbrakk>dynlookup G statT dynC sig = x;
  2115            \<lbrakk>statT = NullT       ; empty sig = x                  \<rbrakk> \<Longrightarrow> P;
  2116   \<And> I.    \<lbrakk>statT = IfaceT I    ; dynimethd G I      dynC sig = x\<rbrakk> \<Longrightarrow> P;
  2117   \<And> statC.\<lbrakk>statT = ClassT statC; dynmethd  G statC  dynC sig = x\<rbrakk> \<Longrightarrow> P;
  2118   \<And> ty.   \<lbrakk>statT = ArrayT ty   ; dynmethd  G Object dynC sig = x\<rbrakk> \<Longrightarrow> P
  2119  \<rbrakk> \<Longrightarrow> P"
  2120 by (cases statT) (auto simp add: dynlookup_def)
  2121 
  2122 subsection "fields"
  2123 
  2124 lemma fields_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
  2125   fields G C = map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c) @  
  2126   (if C = Object then [] else fields G (super c))"
  2127 apply (simp only: fields_def)
  2128 apply (erule class_rec [THEN trans])
  2129 apply assumption
  2130 apply clarsimp
  2131 done
  2132 
  2133 (* local lemma *)
  2134 lemma fields_norec: 
  2135 "\<lbrakk>class G fd = Some c; ws_prog G;  table_of (cfields c) fn = Some f\<rbrakk> 
  2136  \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
  2137 apply (subst fields_rec)
  2138 apply assumption+
  2139 apply (subst map_of_append)
  2140 apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
  2141 apply (auto elim: table_of_map2_SomeI)
  2142 done
  2143 
  2144 (* local lemma *)
  2145 lemma table_of_fieldsD:
  2146 "table_of (map (\<lambda>(fn,ft). ((fn,C),ft)) (cfields c)) efn = Some f
  2147 \<Longrightarrow> (declclassf efn) = C \<and> table_of (cfields c) (fname efn) = Some f"
  2148 apply (case_tac "efn")
  2149 by auto
  2150 
  2151 lemma fields_declC: 
  2152  "\<lbrakk>table_of (fields G C) efn = Some f; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow>  
  2153   (\<exists>d. class G (declclassf efn) = Some d \<and> 
  2154                     table_of (cfields d) (fname efn)=Some f) \<and> 
  2155   G\<turnstile>C \<preceq>\<^sub>C (declclassf efn)  \<and> table_of (fields G (declclassf efn)) efn = Some f"
  2156 apply (erule rev_mp)
  2157 apply (rule ws_subcls1_induct, assumption, assumption)
  2158 apply (subst fields_rec, assumption)
  2159 apply clarify
  2160 apply (simp only: map_of_append)
  2161 apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
  2162 apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
  2163 
  2164 apply   (frule_tac fd="Ca" in fields_norec)
  2165 apply     assumption
  2166 apply     blast
  2167 apply   (frule table_of_fieldsD)  
  2168 apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
  2169               and  m="table_of (if Ca = Object then [] else fields G (super c))"
  2170          in map_add_find_right)
  2171 apply   (case_tac "efn")
  2172 apply   (simp)
  2173 done
  2174 
  2175 lemma fields_emptyI: "\<And>y. \<lbrakk>ws_prog G; class G C = Some c;cfields c = [];  
  2176   C \<noteq> Object \<longrightarrow> class G (super c) = Some y \<and> fields G (super c) = []\<rbrakk> \<Longrightarrow>  
  2177   fields G C = []"
  2178 apply (subst fields_rec)
  2179 apply assumption
  2180 apply auto
  2181 done
  2182 
  2183 (* easier than with table_of *)
  2184 lemma fields_mono_lemma: 
  2185 "\<lbrakk>x \<in> set (fields G C); G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> 
  2186  \<Longrightarrow> x \<in> set (fields G D)"
  2187 apply (erule rev_mp)
  2188 apply (erule converse_rtrancl_induct)
  2189 apply  fast
  2190 apply (drule subcls1D)
  2191 apply clarsimp
  2192 apply (subst fields_rec)
  2193 apply   auto
  2194 done
  2195 
  2196 
  2197 lemma ws_unique_fields_lemma: 
  2198  "\<lbrakk>(efn,fd)  \<in> set (fields G (super c)); fc \<in> set (cfields c); ws_prog G;  
  2199    fname efn = fname fc; declclassf efn = C;
  2200    class G C = Some c; C \<noteq> Object; class G (super c) = Some d\<rbrakk> \<Longrightarrow> R"
  2201 apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption)
  2202 apply (drule_tac weak_map_of_SomeI)
  2203 apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption)
  2204 apply (auto dest: fields_declC [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]])
  2205 done
  2206 
  2207 lemma ws_unique_fields: "\<lbrakk>is_class G C; ws_prog G; 
  2208        \<And>C c. \<lbrakk>class G C = Some c\<rbrakk> \<Longrightarrow> unique (cfields c) \<rbrakk> \<Longrightarrow>
  2209       unique (fields G C)" 
  2210 apply (rule ws_subcls1_induct, assumption, assumption)
  2211 apply (subst fields_rec, assumption)            
  2212 apply (auto intro!: unique_map_inj inj_onI 
  2213             elim!: unique_append ws_unique_fields_lemma fields_norec)
  2214 done
  2215 
  2216 
  2217 subsection "accfield"
  2218 
  2219 lemma accfield_fields: 
  2220  "accfield G S C fn = Some f 
  2221   \<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
  2222 apply (simp only: accfield_def Let_def)
  2223 apply (rule table_of_remap_SomeD)
  2224 apply (auto dest: filter_tab_SomeD)
  2225 done
  2226 
  2227 
  2228 lemma accfield_declC_is_class: 
  2229  "\<lbrakk>is_class G C; accfield G S C en = Some (fd, f); ws_prog G\<rbrakk> \<Longrightarrow>  
  2230    is_class G fd"
  2231 apply (drule accfield_fields)
  2232 apply (drule fields_declC [THEN conjunct1], assumption)
  2233 apply auto
  2234 done
  2235 
  2236 lemma accfield_accessibleD: 
  2237   "accfield G S C fn = Some f \<Longrightarrow> G\<turnstile>Field fn f of C accessible_from S"
  2238 by (auto simp add: accfield_def Let_def)
  2239 
  2240 subsection "is methd"
  2241 
  2242 lemma is_methdI: 
  2243 "\<lbrakk>class G C = Some y; methd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig"
  2244 apply (unfold is_methd_def)
  2245 apply auto
  2246 done
  2247 
  2248 lemma is_methdD: 
  2249 "is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> methd G C sig \<noteq> None"
  2250 apply (unfold is_methd_def)
  2251 apply auto
  2252 done
  2253 
  2254 lemma finite_is_methd: 
  2255  "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
  2256 apply (unfold is_methd_def)
  2257 apply (subst SetCompr_Sigma_eq)
  2258 apply (rule finite_is_class [THEN finite_SigmaI])
  2259 apply (simp only: mem_Collect_eq)
  2260 apply (fold dom_def)
  2261 apply (erule finite_dom_methd)
  2262 apply assumption
  2263 done
  2264 
  2265 section "calculation of the superclasses of a class"
  2266 
  2267 constdefs 
  2268  superclasses:: "prog \<Rightarrow> qtname \<Rightarrow> qtname set"
  2269  "superclasses G C \<equiv> class_rec (G,C) {} 
  2270                        (\<lambda> C c superclss. (if C=Object 
  2271                                             then {} 
  2272                                             else insert (super c) superclss))"
  2273    
  2274 lemma superclasses_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
  2275  superclasses G C 
  2276  = (if (C=Object) 
  2277        then {}
  2278        else insert (super c) (superclasses G (super c)))"
  2279 apply (unfold superclasses_def)
  2280 apply (erule class_rec [THEN trans], assumption)
  2281 apply (simp)
  2282 done
  2283 
  2284 lemma superclasses_mono:
  2285 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
  2286   \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc;
  2287   x\<in>superclasses G D 
  2288 \<rbrakk> \<Longrightarrow> x\<in>superclasses G C" 
  2289 proof -
  2290   
  2291   assume     ws: "ws_prog G"          and 
  2292           cls_C: "class G C = Some c" and
  2293              wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
  2294                   \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
  2295   assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
  2296   thus "\<And> c. \<lbrakk>class G C = Some c; x\<in>superclasses G D\<rbrakk>\<Longrightarrow>
  2297         x\<in>superclasses G C" (is "PROP ?P C"  
  2298                              is "\<And> c. ?CLS C c \<Longrightarrow> ?SUP D \<Longrightarrow> ?SUP C")
  2299   proof (induct ?P C  rule: converse_trancl_induct)
  2300     fix C c
  2301     assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1D" "class G C = Some c" "x \<in> superclasses G D"
  2302     with wf ws show "?SUP C"
  2303       by (auto    intro: no_subcls1_Object 
  2304                simp add: superclasses_rec subcls1_def)
  2305   next
  2306     fix C S c
  2307     assume clsrel': "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S \<prec>\<^sub>C D"
  2308        and    hyp : "\<And> s. \<lbrakk>class G S = Some s; x \<in> superclasses G D\<rbrakk>
  2309                            \<Longrightarrow> x \<in> superclasses G S"
  2310        and  cls_C': "class G C = Some c"
  2311        and       x: "x \<in> superclasses G D"
  2312     moreover note wf ws
  2313     moreover from calculation 
  2314     have "?SUP S" 
  2315       by (force intro: no_subcls1_Object simp add: subcls1_def)
  2316     moreover from calculation 
  2317     have "super c = S" 
  2318       by (auto intro: no_subcls1_Object simp add: subcls1_def)
  2319     ultimately show "?SUP C" 
  2320       by (auto intro: no_subcls1_Object simp add: superclasses_rec)
  2321   qed
  2322 qed
  2323 
  2324 lemma subclsEval:
  2325 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D;ws_prog G; class G C = Some c;
  2326   \<And> C c. \<lbrakk>class G C = Some c;C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class G (super c) = Some sc 
  2327  \<rbrakk> \<Longrightarrow> D\<in>superclasses G C" 
  2328 proof -
  2329   note converse_trancl_induct 
  2330        = converse_trancl_induct [consumes 1,case_names Single Step]
  2331   assume 
  2332              ws: "ws_prog G"          and 
  2333           cls_C: "class G C = Some c" and
  2334              wf: "\<And>C c. \<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk>
  2335                   \<Longrightarrow> \<exists>sc. class G (super c) = Some sc"
  2336   assume clsrel: "G\<turnstile>C\<prec>\<^sub>C D"           
  2337   thus "\<And> c. class G C = Some c\<Longrightarrow> D\<in>superclasses G C" 
  2338     (is "PROP ?P C"  is "\<And> c. ?CLS C c  \<Longrightarrow> ?SUP C")
  2339   proof (induct ?P C  rule: converse_trancl_induct)
  2340     fix C c
  2341     assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" "class G C = Some c"
  2342     with ws wf show "?SUP C"
  2343       by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
  2344   next
  2345     fix C S c
  2346     assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" "G\<turnstile>S\<prec>\<^sub>C D" 
  2347            "\<And>s. class G S = Some s \<Longrightarrow> D \<in> superclasses G S"
  2348            "class G C = Some c" 
  2349     with ws wf show "?SUP C"
  2350       by - (rule superclasses_mono,
  2351             auto dest: no_subcls1_Object simp add: subcls1_def )
  2352   qed
  2353 qed
  2354 
  2355 end