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