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