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