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