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