Theory DeclConcepts

(*  Title:      HOL/Bali/DeclConcepts.thy
    Author:     Norbert Schirmer
*)
subsection ‹Advanced concepts on Java declarations like overriding, inheritance,
dynamic method lookup›

theory DeclConcepts imports TypeRel begin

subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"

definition is_public :: "prog  qtname  bool" where
"is_public G qn = (case class G qn of
                     None        (case iface G qn of
                                      None        False
                                    | Some i  access i = Public)
                   | Some c  access c = Public)"

subsection "accessibility of types (cf. 6.6.1)"
text ‹
Primitive types are always accessible, interfaces and classes are accessible
in their package or if they are defined public, an array type is accessible if
its element type is accessible›
 
primrec
  accessible_in :: "prog  ty  pname  bool"  ("_  _ accessible'_in _" [61,61,61] 60) and
  rt_accessible_in :: "prog  ref_ty  pname  bool"  ("_  _ accessible'_in'' _" [61,61,61] 60)
where
  "G(PrimT p) accessible_in pack = True"
| accessible_in_RefT_simp:
  "G(RefT  r) accessible_in pack = Gr accessible_in' pack"
| "G(NullT) accessible_in' pack = True"
| "G(IfaceT I) accessible_in' pack = ((pid I = pack)  is_public G I)"
| "G(ClassT C) accessible_in' pack = ((pid C = pack)  is_public G C)"
| "G(ArrayT ty) accessible_in' pack = Gty accessible_in pack"

declare accessible_in_RefT_simp [simp del]

definition
  is_acc_class :: "prog  pname  qtname  bool"
  where "is_acc_class G P C = (is_class G C  G(Class C) accessible_in P)"

definition
  is_acc_iface :: "prog  pname  qtname  bool"
  where "is_acc_iface G P I = (is_iface G I  G(Iface I) accessible_in P)"

definition
  is_acc_type :: "prog  pname  ty  bool"
  where "is_acc_type  G P T = (is_type G T   GT accessible_in P)"

definition
  is_acc_reftype  :: "prog  pname  ref_ty  bool"
  where "is_acc_reftype G P T = (isrtype G T   GT accessible_in' P)"

lemma is_acc_classD:
 "is_acc_class G P C   is_class G C  G(Class C) accessible_in P"
by (simp add: is_acc_class_def)

lemma is_acc_class_is_class: "is_acc_class G P C  is_class G C"
by (auto simp add: is_acc_class_def)

lemma is_acc_ifaceD:
  "is_acc_iface G P I  is_iface G I  G(Iface I) accessible_in P"
by (simp add: is_acc_iface_def)

lemma is_acc_typeD:
 "is_acc_type  G P T  is_type G T   GT accessible_in P"
by (simp add: is_acc_type_def)

lemma is_acc_reftypeD:
"is_acc_reftype  G P T  isrtype G T   GT accessible_in' P"
by (simp add: is_acc_reftype_def)

subsection "accessibility of members"
text ‹
The accessibility of members is more involved as the accessibility of types.
We have to distinguish several cases to model the different effects of 
accessibility during inheritance, overriding and ordinary member access 
›

subsubsection ‹Various technical conversion and selection functions›

text ‹overloaded selector accmodi› to select the access modifier 
out of various HOL types›

class has_accmodi =
  fixes accmodi:: "'a  acc_modi"

instantiation acc_modi :: has_accmodi
begin

definition
  acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"

instance ..

end

lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
by (simp add: acc_modi_accmodi_def)

instantiation decl_ext :: (type) has_accmodi
begin

definition
  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"

instance ..

end

lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
by (simp add: decl_acc_modi_def)

instantiation prod :: (type, has_accmodi) has_accmodi
begin

definition
  pair_acc_modi_def: "accmodi p = accmodi (snd p)"

instance ..

end

lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
by (simp add: pair_acc_modi_def)

instantiation memberdecl :: has_accmodi
begin

definition
  memberdecl_acc_modi_def: "accmodi m = (case m of
                                          fdecl f  accmodi f
                                        | mdecl m  accmodi m)"

instance ..

end

lemma memberdecl_fdecl_acc_modi_simp[simp]:
 "accmodi (fdecl m) = accmodi m"
by (simp add: memberdecl_acc_modi_def)

lemma memberdecl_mdecl_acc_modi_simp[simp]:
 "accmodi (mdecl m) = accmodi m"
by (simp add: memberdecl_acc_modi_def)

text ‹overloaded selector declclass› to select the declaring class 
out of various HOL types›

class has_declclass =
  fixes declclass:: "'a  qtname"

instantiation qtname_ext :: (type) has_declclass
begin

definition
  "declclass q =  pid = pid q, tid = tid q "

instance ..

end

lemma qtname_declclass_def:
  "declclass q  (q::qtname)"
  by (induct q) (simp add: declclass_qtname_ext_def)

lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
by (simp add: qtname_declclass_def)

instantiation prod :: (has_declclass, type) has_declclass
begin

definition
  pair_declclass_def: "declclass p = declclass (fst p)"

instance ..

end

lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
by (simp add: pair_declclass_def)

text ‹overloaded selector is_static› to select the static modifier 
out of various HOL types›

class has_static =
  fixes is_static :: "'a  bool"

instantiation decl_ext :: (has_static) has_static
begin

instance ..

end

instantiation member_ext :: (type) has_static
begin

instance ..

end

axiomatization where
  static_field_type_is_static_def: "is_static (m::('a member_scheme))  static m"

lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
by (simp add: static_field_type_is_static_def)

instantiation prod :: (type, has_static) has_static
begin

definition
  pair_is_static_def: "is_static p = is_static (snd p)"

instance ..

end

lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
by (simp add: pair_is_static_def)

lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
by (simp add: pair_is_static_def)

instantiation memberdecl :: has_static
begin

definition
memberdecl_is_static_def: 
 "is_static m = (case m of
                    fdecl f  is_static f
                  | mdecl m  is_static m)"

instance ..

end

lemma memberdecl_is_static_fdecl_simp[simp]:
 "is_static (fdecl f) = is_static f"
by (simp add: memberdecl_is_static_def)

lemma memberdecl_is_static_mdecl_simp[simp]:
 "is_static (mdecl m) = is_static m"
by (simp add: memberdecl_is_static_def)

lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
by (cases m) (simp add: mhead_def member_is_static_simp)

― ‹some mnemotic selectors for various pairs› 

definition
  decliface :: "qtname × 'a decl_scheme  qtname" where
  "decliface = fst"          ― ‹get the interface component›

definition
  mbr :: "qtname × memberdecl  memberdecl" where
  "mbr = snd"            ― ‹get the memberdecl component›

definition
  mthd :: "'b × 'a  'a" where
  "mthd = snd"              ― ‹get the method component›
    ― ‹also used for mdecl, mhead›

definition
  fld :: "'b × 'a decl_scheme  'a decl_scheme" where
  "fld = snd"               ― ‹get the field component›
    ― ‹also used for ((vname × qtname)× field)›

― ‹some mnemotic selectors for (vname × qtname)›

definition
  fname:: "vname × 'a  vname"
  where "fname = fst"
    ― ‹also used for fdecl›

definition
  declclassf:: "(vname × qtname)  qtname"
  where "declclassf = snd"


lemma decliface_simp[simp]: "decliface (I,m) = I"
by (simp add: decliface_def) 

lemma mbr_simp[simp]: "mbr (C,m) = m"
by (simp add: mbr_def)

lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m"
by (cases m) (simp add:  mbr_def) 

lemma mthd_simp[simp]: "mthd (C,m) = m"
by (simp add: mthd_def)

lemma fld_simp[simp]: "fld (C,f) = f"
by (simp add: fld_def)

lemma accmodi_simp[simp]: "accmodi (C,m) = access m"
by (simp )

lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m"
by (cases m) (simp add: mthd_def) 

lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f"
by (cases f) (simp add:  fld_def) 

lemma static_mthd_simp[simp]: "static (mthd m) = is_static m"
by (cases m) (simp add:  mthd_def member_is_static_simp)

lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m"
by (cases m) simp

lemma static_fld_simp[simp]: "static (fld f) = is_static f"
by (cases f) (simp add:  fld_def member_is_static_simp)

lemma ext_field_simp [simp]: "(declclass f,fld f) = f"
by (cases f) (simp add:  fld_def)

lemma ext_method_simp [simp]: "(declclass m,mthd m) = m"
by (cases m) (simp add:  mthd_def)

lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m"
by (cases m) (simp add: mbr_def)

lemma fname_simp[simp]:"fname (n,c) = n"
by (simp add: fname_def)

lemma declclassf_simp[simp]:"declclassf (n,c) = c"
by (simp add: declclassf_def)

  ― ‹some mnemotic selectors for (vname × qtname)›

definition
  fldname :: "vname × qtname  vname"
  where "fldname = fst"

definition
  fldclass :: "vname × qtname  qtname"
  where "fldclass = snd"

lemma fldname_simp[simp]: "fldname (n,c) = n"
by (simp add: fldname_def)

lemma fldclass_simp[simp]: "fldclass (n,c) = c"
by (simp add: fldclass_def)

lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
by (simp add: fldname_def fldclass_def)

text ‹Convert a qualified method declaration (qualified with its declaring 
class) to a qualified member declaration:  methdMembr›

definition
  methdMembr :: "qtname × mdecl  qtname × memberdecl"
  where "methdMembr m = (fst m, mdecl (snd m))"

lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
by (simp add: methdMembr_def)

lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m"
by (cases m) (simp add: methdMembr_def)

lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m"
by (cases m) (simp add: methdMembr_def)

lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
by (cases m) (simp add: methdMembr_def)

text ‹Convert a qualified method (qualified with its declaring 
class) to a qualified member declaration:  method›

definition
  "method" :: "sig  (qtname × methd)  (qtname × memberdecl)"
  where "method sig m = (declclass m, mdecl (sig, mthd m))"

lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
by (simp add: method_def)

lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m"
by (simp add: method_def)

lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m"
by (simp add: method_def)

lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m"
by (cases m) (simp add: method_def)

lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)"
by (simp add: mbr_def method_def)

lemma memberid_method_simp[simp]:  "memberid (method sig m) = mid sig"
  by (simp add: method_def) 

definition
  fieldm :: "vname  (qtname × field)  (qtname × memberdecl)"
  where "fieldm n f = (declclass f, fdecl (n, fld f))"

lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
by (simp add: fieldm_def)

lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f"
by (simp add: fieldm_def)

lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f"
by (simp add: fieldm_def)

lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f"
by (cases f) (simp add: fieldm_def)

lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)"
by (simp add: mbr_def fieldm_def)

lemma memberid_fieldm_simp[simp]:  "memberid (fieldm n f) = fid n"
by (simp add: fieldm_def) 

text ‹Select the signature out of a qualified method declaration:
 msig›

definition
  msig :: "(qtname × mdecl)  sig"
  where "msig m = fst (snd m)"

lemma msig_simp[simp]: "msig (c,(s,m)) = s"
by (simp add: msig_def)

text ‹Convert a qualified method (qualified with its declaring 
class) to a qualified method declaration:  qmdecl›

definition
  qmdecl :: "sig  (qtname × methd)  (qtname × mdecl)"
  where "qmdecl sig m = (declclass m, (sig,mthd m))"

lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
by (simp add: qmdecl_def)

lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m"
by (simp add: qmdecl_def)

lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m"
by (simp add: qmdecl_def)

lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m"
by (cases m) (simp add: qmdecl_def)

lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig"
by (simp add: qmdecl_def)

lemma mdecl_qmdecl_simp[simp]:  
 "mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 
by (simp add: qmdecl_def) 

lemma methdMembr_qmdecl_simp [simp]: 
 "methdMembr (qmdecl sig old) = method sig old"
by (simp add: methdMembr_def qmdecl_def method_def)

text ‹overloaded selector resTy› to select the result type 
out of various HOL types›

class has_resTy =
  fixes resTy:: "'a  ty"

instantiation decl_ext :: (has_resTy) has_resTy
begin

instance ..

end

instantiation member_ext :: (has_resTy) has_resTy
begin

instance ..

end

instantiation mhead_ext :: (type) has_resTy
begin

instance ..

end

axiomatization where
  mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme))  resT m"

lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
by (simp add: mhead_ext_type_resTy_def)

lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
by (simp add: mhead_def mhead_resTy_simp)

instantiation prod :: (type, has_resTy) has_resTy
begin

definition
  pair_resTy_def: "resTy p = resTy (snd p)"

instance ..

end

lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
by (simp add: pair_resTy_def)

lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m"
by (cases m) (simp)

lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m"
by (cases m) (simp add: mthd_def )

subsubsection "inheritable-in"
text G⊢m inheritable_in P›: m can be inherited by
classes in package P if:
\begin{itemize} 
\item the declaration class of m is accessible in P and
\item the member m is declared with protected or public access or if it is
      declared with default (package) access, the package of the declaration 
      class of m is also P. If the member m is declared with private access
      it is not accessible for inheritance at all.
\end{itemize}
›
definition
  inheritable_in :: "prog  (qtname × memberdecl)  pname  bool" ("_  _ inheritable'_in _" [61,61,61] 60)
where
"Gmembr inheritable_in pack =
  (case (accmodi membr) of
     Private    False
   | Package    (pid (declclass membr)) = pack
   | Protected  True
   | Public     True)"

abbreviation
Method_inheritable_in_syntax::
 "prog  (qtname × mdecl)  pname  bool"
                ("_ ⊢Method _ inheritable'_in _ " [61,61,61] 60)
 where "G⊢Method m inheritable_in p == GmethdMembr m inheritable_in p"

abbreviation
Methd_inheritable_in::
 "prog  sig  (qtname × methd)  pname  bool"
                ("_ ⊢Methd _ _ inheritable'_in _ " [61,61,61,61] 60)
 where "G⊢Methd s m inheritable_in p == G(method s m) inheritable_in p"

subsubsection "declared-in/undeclared-in"

definition
  cdeclaredmethd :: "prog  qtname  (sig,methd) table" where
  "cdeclaredmethd G C =
    (case class G C of
       None  λ sig. None
     | Some c  table_of (methods c))"

definition
  cdeclaredfield :: "prog  qtname  (vname,field) table" where
  "cdeclaredfield G C =
    (case class G C of
      None  λ sig. None
    | Some c  table_of (cfields c))"

definition
  declared_in :: "prog   memberdecl  qtname  bool" ("_ _ declared'_in _" [61,61,61] 60)
where
  "Gm declared_in C = (case m of
                          fdecl (fn,f )  cdeclaredfield G C fn  = Some f
                        | mdecl (sig,m)  cdeclaredmethd G C sig = Some m)"

abbreviation
method_declared_in:: "prog   (qtname × mdecl)  qtname  bool"
                                 ("_⊢Method _ declared'_in _" [61,61,61] 60)
 where "G⊢Method m declared_in C == Gmdecl (mthd m) declared_in C"

abbreviation
methd_declared_in:: "prog   sig  (qtname × methd)  qtname  bool"
                               ("_⊢Methd _  _ declared'_in _" [61,61,61,61] 60)
 where "G⊢Methd s m declared_in C == Gmdecl (s,mthd m) declared_in C"

lemma declared_in_classD:
 "Gm declared_in C  is_class G C"
by (cases m) 
   (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)

definition
  undeclared_in :: "prog   memberid  qtname  bool" ("_ _ undeclared'_in _" [61,61,61] 60)
where
  "Gm undeclared_in C = (case m of
                           fid fn   cdeclaredfield G C fn  = None
                         | mid sig  cdeclaredmethd G C sig = None)"


subsubsection "members"

(* Can't just take a function: prog ⇒ qtname ⇒ memberdecl set because
   the class qtname changes to the superclass in the inductive definition
   below
*)

inductive
  members :: "prog  (qtname × memberdecl)  qtname  bool"
    ("_  _ member'_of _" [61,61,61] 60)
  for G :: prog
where

  Immediate: "Gmbr m declared_in C;declclass m = C  Gm member_of C"
| Inherited: "Gm inheritable_in (pid C); Gmemberid m undeclared_in C; 
               GC C1 S; G(Class S) accessible_in (pid C);Gm member_of S 
                Gm member_of C"
text ‹Note that in the case of an inherited member only the members of the
direct superclass are concerned. If a member of a superclass of the direct
superclass isn't inherited in the direct superclass (not member of the
direct superclass) than it can't be a member of the class. E.g. If a
member of a class A is defined with package access it isn't member of a 
subclass S if S isn't in the same package as A. Any further subclasses 
of S will not inherit the member, regardless if they are in the same
package as A or not.›

abbreviation
method_member_of:: "prog  (qtname × mdecl)  qtname  bool"
                           ("_ ⊢Method _ member'_of _" [61,61,61] 60)
 where "G⊢Method m member_of C == G(methdMembr m) member_of C"

abbreviation
methd_member_of:: "prog  sig  (qtname × methd)  qtname  bool"
                           ("_ ⊢Methd _ _ member'_of _" [61,61,61,61] 60)
 where "G⊢Methd s m member_of C == G(method s m) member_of C" 

abbreviation
fieldm_member_of:: "prog  vname  (qtname × field)  qtname  bool"
                           ("_ ⊢Field _  _ member'_of _" [61,61,61] 60)
 where "G⊢Field n f member_of C == Gfieldm n f member_of C"

definition
  inherits :: "prog  qtname  (qtname × memberdecl)  bool" ("_  _ inherits _" [61,61,61] 60)
where
  "GC inherits m =
    (Gm inheritable_in (pid C)  Gmemberid m undeclared_in C  
      (S. GC C1 S  G(Class S) accessible_in (pid C)  Gm member_of S))"

lemma inherits_member: "GC inherits m  Gm member_of C"
by (auto simp add: inherits_def intro: members.Inherited)


definition
  member_in :: "prog  (qtname × memberdecl)  qtname  bool" ("_  _ member'_in _" [61,61,61] 60)
  where "Gm member_in C = ( provC. G C C provC  G  m member_of provC)"
text ‹A member is in a class if it is member of the class or a superclass.
If a member is in a class we can select this member. This additional notion
is necessary since not all members are inherited to subclasses. So such
members are not member-of the subclass but member-in the subclass.›

abbreviation
method_member_in:: "prog  (qtname × mdecl)  qtname  bool"
                           ("_ ⊢Method _ member'_in _" [61,61,61] 60)
 where "G⊢Method m member_in C == G(methdMembr m) member_in C"

abbreviation
methd_member_in:: "prog  sig  (qtname × methd)  qtname  bool"
                           ("_ ⊢Methd _ _ member'_in _" [61,61,61,61] 60)
 where "G⊢Methd s m member_in C == G(method s m) member_in C"

lemma member_inD: "Gm member_in C 
   provC. G C C provC  G  m member_of provC"
by (auto simp add: member_in_def)

lemma member_inI: "G  m member_of provC;G C C provC   Gm member_in C"
by (auto simp add: member_in_def)

lemma member_of_to_member_in: "G  m member_of C  G m member_in C"
by (auto intro: member_inI)


subsubsection "overriding"

text ‹Unfortunately the static notion of overriding (used during the
typecheck of the compiler) and the dynamic notion of overriding (used during
execution in the JVM) are not exactly the same. 
›

text ‹Static overriding (used during the typecheck of the compiler)›

inductive
  stat_overridesR :: "prog  (qtname × mdecl)  (qtname × mdecl)  bool"
    ("_  _ overridesS _" [61,61,61] 60)
  for G :: prog
where

  Direct: "¬ is_static new; msig new = msig old; 
           G⊢Method new declared_in (declclass new);  
           G⊢Method old declared_in (declclass old); 
           G⊢Method old inheritable_in pid (declclass new);
           G(declclass new) C1 superNew;
           G ⊢Method old member_of superNew
             Gnew overridesS old"

| Indirect: "Gnew overridesS intr; Gintr overridesS old
              Gnew overridesS old"

text ‹Dynamic overriding (used during the typecheck of the compiler)›

inductive
  overridesR :: "prog  (qtname × mdecl)  (qtname × mdecl)  bool"
    ("_  _ overrides _" [61,61,61] 60)
  for G :: prog
where

  Direct: "¬ is_static new; ¬ is_static old; accmodi new  Private;
           msig new = msig old; 
           G(declclass new) C (declclass old);
           G⊢Method new declared_in (declclass new);  
           G⊢Method old declared_in (declclass old);    
           G⊢Method old inheritable_in pid (declclass new);
           GresTy new  resTy old
             Gnew overrides old"

| Indirect: "Gnew overrides intr; Gintr overrides old
             Gnew overrides old"

abbreviation (input)
sig_stat_overrides:: 
 "prog   sig  (qtname × methd)  (qtname × methd)  bool" 
                                  ("_,_ _ overridesS _" [61,61,61,61] 60)
 where "G,snew overridesS old == G(qmdecl s new) overridesS (qmdecl s old)" 

abbreviation (input)
sig_overrides:: "prog   sig  (qtname × methd)  (qtname × methd)  bool" 
                                  ("_,_ _ overrides _" [61,61,61,61] 60)
 where "G,snew overrides old == G(qmdecl s new) overrides (qmdecl s old)"

subsubsection "Hiding"

definition
  hides :: "prog  (qtname × mdecl)  (qtname × mdecl)  bool" ("_ _ hides _" [61,61,61] 60)
where 
  "Gnew hides old =
    (is_static new  msig new = msig old 
      G(declclass new) C (declclass old) 
      G⊢Method new declared_in (declclass new) 
      G⊢Method old declared_in (declclass old)  
      G⊢Method old inheritable_in pid (declclass new))"

abbreviation
sig_hides:: "prog   sig  (qtname × methd)  (qtname × methd)  bool" 
                                  ("_,_ _ hides _" [61,61,61,61] 60)
 where "G,snew hides old == G(qmdecl s new) hides (qmdecl s old)"

lemma hidesI:
"is_static new; msig new = msig old;
  G(declclass new) C (declclass old);
  G⊢Method new declared_in (declclass new);
  G⊢Method old declared_in (declclass old);
  G⊢Method old inheritable_in pid (declclass new)
   Gnew hides old"
by (auto simp add: hides_def)

lemma hidesD:
"Gnew hides old   
  declclass new  Object  is_static new  msig new = msig old  
  G(declclass new) C (declclass old) 
  G⊢Method new declared_in (declclass new)    
  G⊢Method old declared_in (declclass old)"
by (auto simp add: hides_def)

lemma overrides_commonD:
"Gnew overrides old   
  declclass new  Object  ¬ is_static new  ¬ is_static old 
  accmodi new  Private  
  msig new = msig old  
  G(declclass new) C (declclass old) 
  G⊢Method new declared_in (declclass new)    
  G⊢Method old declared_in (declclass old)"
by (induct set: overridesR) (auto intro: trancl_trans)

lemma ws_overrides_commonD:
"Gnew overrides old;ws_prog G   
  declclass new  Object  ¬ is_static new  ¬ is_static old 
  accmodi new  Private  GresTy new  resTy old 
  msig new = msig old  
  G(declclass new) C (declclass old) 
  G⊢Method new declared_in (declclass new)    
  G⊢Method old declared_in (declclass old)"
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans)

lemma overrides_eq_sigD: 
 "Gnew overrides old  msig old=msig new"
by (auto dest: overrides_commonD)

lemma hides_eq_sigD: 
 "Gnew hides old  msig old=msig new"
by (auto simp add: hides_def)

subsubsection "permits access" 
definition
  permits_acc :: "prog  (qtname × memberdecl)  qtname  qtname  bool" ("_  _ in _ permits'_acc'_from _" [61,61,61,61] 60)
where
  "Gmembr in cls permits_acc_from accclass =
    (case (accmodi membr) of
      Private    (declclass membr = accclass)
    | Package    (pid (declclass membr) = pid accclass)
    | Protected  (pid (declclass membr) = pid accclass)
                    
                    (Gaccclass C declclass membr 
                      (Gcls C accclass  is_static membr)) 
    | Public     True)"
text ‹
The subcondition of the termProtected case: 
termGaccclass C declclass membr could also be relaxed to:
termGaccclass C declclass membr since in case both classes are the
same the other condition term(pid (declclass membr) = pid accclass)
holds anyway.
› 

text ‹Like in case of overriding, the static and dynamic accessibility 
of members is not uniform.
\begin{itemize}
\item Statically the class/interface of the member must be accessible for the
      member to be accessible. During runtime this is not necessary. For
      Example, if a class is accessible and we are allowed to access a member
      of this class (statically) we expect that we can access this member in 
      an arbitrary subclass (during runtime). It's not intended to restrict
      the access to accessible subclasses during runtime.
\item Statically the member we want to access must be "member of" the class.
      Dynamically it must only be "member in" the class.
\end{itemize} 
› 

inductive
  accessible_fromR :: "prog  qtname  (qtname × memberdecl)  qtname  bool"
  and accessible_from :: "prog  (qtname × memberdecl)  qtname  qtname  bool"
    ("_  _ of _ accessible'_from _" [61,61,61,61] 60)
  and method_accessible_from :: "prog  (qtname × mdecl)  qtname  qtname  bool"
    ("_ ⊢Method _ of _ accessible'_from _" [61,61,61,61] 60)
  for G :: prog and accclass :: qtname
where
  "Gmembr of cls accessible_from accclass  accessible_fromR G accclass membr cls"

| "G⊢Method m of cls accessible_from accclass  accessible_fromR G accclass (methdMembr m) cls"

| Immediate:  "!!membr class.
               Gmembr member_of class;
                G(Class class) accessible_in (pid accclass);
                Gmembr in class permits_acc_from accclass 
                 Gmembr of class accessible_from accclass"

| Overriding: "!!membr class C new old supr.
               Gmembr member_of class;
                G(Class class) accessible_in (pid accclass);
                membr=(C,mdecl new);
                G(C,new) overridesS old; 
                Gclass C supr;
                G⊢Method old of supr accessible_from accclass
                Gmembr of class accessible_from accclass"

abbreviation
methd_accessible_from:: 
 "prog  sig  (qtname × methd)  qtname  qtname  bool"
                 ("_ ⊢Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60)
 where
 "G⊢Methd s m of cls accessible_from accclass ==
   G(method s m) of cls accessible_from accclass"

abbreviation
field_accessible_from:: 
 "prog  vname  (qtname × field)  qtname  qtname  bool"
                 ("_ ⊢Field _  _ of _ accessible'_from _" [61,61,61,61,61] 60)
 where
 "G⊢Field fn f of C accessible_from accclass ==
  G(fieldm fn f) of C accessible_from accclass"

inductive
  dyn_accessible_fromR :: "prog  qtname  (qtname × memberdecl)  qtname  bool"
  and dyn_accessible_from' ::  "prog  (qtname × memberdecl)  qtname  qtname  bool"
    ("_  _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
  and method_dyn_accessible_from :: "prog  (qtname × mdecl)  qtname  qtname  bool"
    ("_ ⊢Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
  for G :: prog and accclass :: qtname
where
  "Gmembr in C dyn_accessible_from accC  dyn_accessible_fromR G accC membr C"

| "G⊢Method m in C dyn_accessible_from accC  dyn_accessible_fromR G accC (methdMembr m) C"

| Immediate:  "!!class. Gmembr member_in class;
                Gmembr in class permits_acc_from accclass 
                 Gmembr in class dyn_accessible_from accclass"

| Overriding: "!!class. Gmembr member_in class;
                membr=(C,mdecl new);
                G(C,new) overrides old; 
                Gclass C supr;
                G⊢Method old in supr dyn_accessible_from accclass
                Gmembr in class dyn_accessible_from accclass"

abbreviation
methd_dyn_accessible_from:: 
 "prog  sig  (qtname × methd)  qtname  qtname  bool"
             ("_ ⊢Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
 where
 "G⊢Methd s m in C dyn_accessible_from accC ==
  G(method s m) in C dyn_accessible_from accC"  

abbreviation
field_dyn_accessible_from:: 
 "prog  vname  (qtname × field)  qtname  qtname  bool"
         ("_ ⊢Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60)
 where
 "G⊢Field fn f in dynC dyn_accessible_from accC ==
  G(fieldm fn f) in dynC dyn_accessible_from accC"


lemma accessible_from_commonD: "Gm of C accessible_from S
  Gm member_of C  G(Class C) accessible_in (pid S)"
by (auto elim: accessible_fromR.induct)

lemma unique_declaration: 
 "Gm declared_in C;  Gn declared_in C; memberid m = memberid n  
   m = n"
apply (cases m)
apply (cases n,
        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
done

lemma declared_not_undeclared:
  "Gm declared_in C  ¬ G memberid m undeclared_in C"
by (cases m) (auto simp add: declared_in_def undeclared_in_def)

lemma undeclared_not_declared:
 "G memberid m undeclared_in C  ¬ G m declared_in C" 
by (cases m) (auto simp add: declared_in_def undeclared_in_def)

lemma not_undeclared_declared:
  "¬ G membr_id undeclared_in C  ( m. Gm declared_in C  
                                           membr_id = memberid m)"
proof -
  assume not_undecl:"¬ G membr_id undeclared_in C"
  show ?thesis (is "?P membr_id")
  proof (cases membr_id)
    case (fid vname)
    with not_undecl
    obtain fld where
      "Gfdecl (vname,fld) declared_in C" 
      by (auto simp add: undeclared_in_def declared_in_def
                         cdeclaredfield_def)
    with fid show ?thesis 
      by auto
  next
    case (mid sig)
    with not_undecl
    obtain mthd where
      "Gmdecl (sig,mthd) declared_in C" 
      by (auto simp add: undeclared_in_def declared_in_def
                         cdeclaredmethd_def)
    with mid show ?thesis 
      by auto
  qed
qed

lemma unique_declared_in:
 "Gm declared_in C; Gn declared_in C; memberid m = memberid n
  m = n"
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
            split: memberdecl.splits)

lemma unique_member_of: 
  assumes n: "Gn member_of C" and  
          m: "Gm member_of C" and
       eqid: "memberid n = memberid m"
  shows "n=m"
proof -
  from n m eqid  
  show "n=m"
  proof (induct)
    case (Immediate n C)
    assume member_n: "G mbr n declared_in C" "declclass n = C"
    assume eqid: "memberid n = memberid m"
    assume "G  m member_of C"
    then show "n=m"
    proof (cases)
      case Immediate
      with eqid member_n
      show ?thesis
        by (cases n, cases m) 
           (auto simp add: declared_in_def 
                           cdeclaredmethd_def cdeclaredfield_def
                    split: memberdecl.splits)
    next
      case Inherited
      with eqid member_n
      show ?thesis
        by (cases n) (auto dest: declared_not_undeclared)
    qed
  next
    case (Inherited n C S)
    assume undecl: "G memberid n undeclared_in C"
    assume  super: "GCC1S"
    assume    hyp: "G  m member_of S; memberid n = memberid m  n = m"
    assume   eqid: "memberid n = memberid m"
    assume "G  m member_of C"
    then show "n=m"
    proof (cases)
      case Immediate
      then have "G mbr m declared_in C" by simp
      with eqid undecl
      show ?thesis
        by (cases m) (auto dest: declared_not_undeclared)
    next
      case Inherited 
      with super have "G  m member_of S"
        by (auto dest!: subcls1D)
      with eqid hyp
      show ?thesis 
        by blast
    qed
  qed
qed

lemma member_of_is_classD: "Gm member_of C  is_class G C"
proof (induct set: members)
  case (Immediate m C)
  assume "G mbr m declared_in C"
  then show "is_class G C"
    by (cases "mbr m")
       (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
next
  case (Inherited m C S)  
  assume "GCC1S" and "is_class G S"
  then show "is_class G C"
    by - (rule subcls_is_class2,auto)
qed

lemma member_of_declC: 
 "Gm member_of C 
   Gmbr m declared_in (declclass m)"
by (induct set: members) auto

lemma member_of_member_of_declC:
 "Gm member_of C 
   Gm member_of (declclass m)"
by (auto dest: member_of_declC intro: members.Immediate)

lemma member_of_class_relation:
  "Gm member_of C  GC C declclass m"
proof (induct set: members)
  case (Immediate m C)
  then show "GC C declclass m" by simp
next
  case (Inherited m C S)
  then show "GC C declclass m" 
    by (auto dest: r_into_rtrancl intro: rtrancl_trans)
qed

lemma member_in_class_relation:
  "Gm member_in C  GC C declclass m"
by (auto dest: member_inD member_of_class_relation
        intro: rtrancl_trans)

lemma stat_override_declclasses_relation: 
"G(declclass new) C1 superNew; G ⊢Method old member_of superNew 
 G(declclass new) C (declclass old)"
apply (rule trancl_rtrancl_trancl)
apply (erule r_into_trancl)
apply (cases old)
apply (auto dest: member_of_class_relation)
done

lemma stat_overrides_commonD:
"Gnew overridesS old   
  declclass new  Object  ¬ is_static new  msig new = msig old  
  G(declclass new) C (declclass old) 
  G⊢Method new declared_in (declclass new)    
  G⊢Method old declared_in (declclass old)"
apply (induct set: stat_overridesR) 
apply (frule (1) stat_override_declclasses_relation) 
apply (auto intro: trancl_trans)
done

lemma member_of_Package: 
  assumes "Gm member_of C"
    and "accmodi m = Package"
  shows "pid (declclass m) = pid C"
  using assms
proof induct
  case Immediate
  then show ?case by simp
next
  case Inherited
  then show ?case by (auto simp add: inheritable_in_def)
qed

lemma member_in_declC: "Gm member_in C Gm member_in (declclass m)"
proof -
  assume member_in_C:  "Gm member_in C"
  from member_in_C
  obtain provC where
    subclseq_C_provC: "G C C provC" and
     member_of_provC: "G  m member_of provC"
    by (auto simp add: member_in_def)
  from member_of_provC
  have "G  m member_of declclass m"
    by (rule member_of_member_of_declC)
  moreover
  from member_in_C
  have "GC C declclass m"
    by (rule member_in_class_relation)
  ultimately
  show ?thesis
    by (auto simp add: member_in_def)
qed

lemma dyn_accessible_from_commonD: "Gm in C dyn_accessible_from S
  Gm member_in C"
by (auto elim: dyn_accessible_fromR.induct)

lemma no_Private_stat_override: 
 "Gnew overridesS old  accmodi old  Private"
by (induct set:  stat_overridesR) (auto simp add: inheritable_in_def)

lemma no_Private_override: "Gnew overrides old  accmodi old  Private"
by (induct set: overridesR) (auto simp add: inheritable_in_def)

lemma permits_acc_inheritance:
 "Gm in statC permits_acc_from accC; GdynC C statC
    Gm in dynC permits_acc_from accC"
by (cases "accmodi m")
   (auto simp add: permits_acc_def
            intro: subclseq_trans) 

lemma permits_acc_static_declC:
 "Gm in C permits_acc_from accC; Gm member_in C; is_static m
    Gm in (declclass m) permits_acc_from accC"
by (cases "accmodi m") (auto simp add: permits_acc_def)

lemma dyn_accessible_from_static_declC: 
  assumes  acc_C: "Gm in C dyn_accessible_from accC" and
           static: "is_static m"
  shows "Gm in (declclass m) dyn_accessible_from accC"
proof -
  from acc_C static
  show "Gm in (declclass m) dyn_accessible_from accC"
  proof (induct)
    case (Immediate m C)
    then show ?case 
      by (auto intro!: dyn_accessible_fromR.Immediate
                 dest: member_in_declC permits_acc_static_declC) 
  next 
    case (Overriding m C declCNew new old sup)
    then have "¬ is_static m"
      by (auto dest: overrides_commonD)
    moreover
    assume "is_static m"
    ultimately show ?case 
      by contradiction
  qed
qed

lemma field_accessible_fromD:
 "Gmembr of C accessible_from accC;is_field membr 
   Gmembr member_of C 
      G(Class C) accessible_in (pid accC) 
      Gmembr in C permits_acc_from accC"
by (cases set: accessible_fromR)
   (auto simp add: is_field_def split: memberdecl.splits) 

lemma field_accessible_from_permits_acc_inheritance:
"Gmembr of statC accessible_from accC; is_field membr; G  dynC C statC
 Gmembr in dynC permits_acc_from accC"
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)


(*
lemma accessible_Package:
 "⟦G ⊢ m of C accessible_from S;accmodi m = Package;
   ⋀ new old. G⊢new overridesS old ⟹ accmodi old ≤ accmodi new⟧
  ⟹ pid S = pid C ∧ pid C = pid (declclass m)"
proof -
  assume wf: "⋀ new old. G⊢new overridesS old ⟹ accmodi old ≤ accmodi new"
  assume "G ⊢ m of C accessible_from S"
  then show "accmodi m = Package ⟹ pid S = pid C ∧ pid C = pid (declclass m)"
    (is "?Pack m ⟹ ?P C m")
  proof (induct rule: accessible_fromR.induct)
    fix C m
    assume "G⊢m member_of C"
           "G ⊢ m in C permits_acc_from S"
           "accmodi m = Package"      
    then show "?P C m"
      by (auto dest: member_of_Package simp add: permits_acc_def)
  next
    fix declC C new newm old Sup
    assume member_new: "G ⊢ new member_of C" and 
                acc_C: "G ⊢ Class C accessible_in pid S" and
                  new: "new = (declC, mdecl newm)" and
             override: "G ⊢ (declC, newm) overridesS old" and
         subcls_C_Sup: "G⊢C ≺C Sup" and
              acc_old: "G ⊢ methdMembr old of Sup accessible_from S" and
                  hyp: "?Pack (methdMembr old) ⟹ ?P Sup (methdMembr old)" and
          accmodi_new: "accmodi new = Package"
    from override wf 
    have accmodi_weaken: "accmodi old ≤ accmodi newm"
      by (cases old,cases newm) auto
    from override new
    have "accmodi old ≠ Private"
      by (simp add: no_Private_stat_override)
    with accmodi_weaken accmodi_new new
    have accmodi_old: "accmodi old = Package"
      by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 
    with hyp 
    have P_sup: "?P Sup (methdMembr old)"
      by (simp)
    from wf override new accmodi_old accmodi_new
    have eq_pid_new_old: "pid (declclass new) = pid (declclass old)"
      by (auto dest: stat_override_Package) 
    from member_new accmodi_new
    have "pid (declclass new) = pid C"
      by (auto dest: member_of_Package)
    with eq_pid_new_old P_sup show "?P C new"
      by auto
  qed
qed
*)

lemma accessible_fieldD: 
 "Gmembr of C accessible_from accC; is_field membr
  Gmembr member_of C 
     G(Class C) accessible_in (pid accC) 
     Gmembr in C permits_acc_from accC"
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
      


lemma member_of_Private:
"Gm member_of C; accmodi m = Private  declclass m = C"
by (induct set: members) (auto simp add: inheritable_in_def)

lemma member_of_subclseq_declC:
  "Gm member_of C  GC C declclass m"
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)

lemma member_of_inheritance:
  assumes       m: "Gm member_of D" and
     subclseq_D_C: "GD C C" and
     subclseq_C_m: "GC C declclass m" and
               ws: "ws_prog G" 
  shows "Gm member_of C"
proof -
  from m subclseq_D_C subclseq_C_m
  show ?thesis
  proof (induct)
    case (Immediate m D)
    assume "declclass m = D" and
           "GDC C" and "GCC declclass m"
    with ws have "D=C" 
      by (auto intro: subclseq_acyclic)
    with Immediate 
    show "Gm member_of C"
      by (auto intro: members.Immediate)
  next
    case (Inherited m D S)
    assume member_of_D_props: 
            "G  m inheritable_in pid D" 
            "G memberid m undeclared_in D"  
            "G  Class S accessible_in pid D" 
            "G  m member_of S"
    assume super: "GDC1S"
    assume hyp: "GSC C; GCC declclass m  G  m member_of C"
    assume subclseq_C_m: "GCC declclass m"
    assume "GDC C"
    then show "Gm member_of C"
    proof (cases rule: subclseq_cases)
      case Eq
      assume "D=C" 
      with super member_of_D_props 
      show ?thesis
        by (auto intro: members.Inherited)
    next
      case Subcls
      assume "GDC C"
      with super 
      have "GSC C"
        by (auto dest: subcls1D subcls_superD)
      with subclseq_C_m hyp show ?thesis
        by blast
    qed
  qed
qed

lemma member_of_subcls:
  assumes     old: "Gold member_of C" and 
              new: "Gnew member_of D" and
             eqid: "memberid new = memberid old" and
     subclseq_D_C: "GD C C" and 
   subcls_new_old: "Gdeclclass new C declclass old" and
               ws: "ws_prog G"
  shows "GD C C"
proof -
  from old 
  have subclseq_C_old: "GC C declclass old"
    by (auto dest: member_of_subclseq_declC)
  from new 
  have subclseq_D_new: "GD C declclass new"
    by (auto dest: member_of_subclseq_declC)
  from subcls_new_old ws
  have neq_new_old: "newold"
    by (cases new,cases old) (auto dest: subcls_irrefl)
  from subclseq_D_new subclseq_D_C
  have "G(declclass new) C C  GC C (declclass new)" 
    by (rule subcls_compareable)
  then have "G(declclass new) C C"
  proof
    assume "Gdeclclass newC C" then show ?thesis .
  next
    assume "GC C (declclass new)"
    with new subclseq_D_C ws 
    have "Gnew member_of C"
      by (blast intro: member_of_inheritance)
    with eqid old 
    have "new=old"
      by (blast intro: unique_member_of)
    with neq_new_old 
    show ?thesis
      by contradiction
  qed
  then show ?thesis
  proof (cases rule: subclseq_cases)
    case Eq
    assume "declclass new = C"
    with new have "Gnew member_of C"
      by (auto dest: member_of_member_of_declC)
    with eqid old 
    have "new=old"
      by (blast intro: unique_member_of)
    with neq_new_old 
    show ?thesis
      by contradiction
  next
    case Subcls
    assume "Gdeclclass newC C"
    with subclseq_D_new
    show "GDC C"
      by (rule rtrancl_trancl_trancl)
  qed
qed

corollary member_of_overrides_subcls:
 "G⊢Methd sig old member_of C; G⊢Methd sig new member_of D;GD C C;
   G,signew overrides old; ws_prog G
  GD C C"
by (drule overrides_commonD) (auto intro: member_of_subcls)    

corollary member_of_stat_overrides_subcls:
 "G⊢Methd sig old member_of C; G⊢Methd sig new member_of D;GD C C;
   G,signew overridesS old; ws_prog G
  GD C C"
by (drule stat_overrides_commonD) (auto intro: member_of_subcls)    



lemma inherited_field_access: 
  assumes stat_acc: "Gmembr of statC accessible_from accC" and
          is_field: "is_field membr" and 
          subclseq: "G  dynC C statC"
  shows "Gmembr in dynC dyn_accessible_from accC"
proof -
  from stat_acc is_field subclseq 
  show ?thesis
    by (auto dest: accessible_fieldD 
            intro: dyn_accessible_fromR.Immediate 
                   member_inI 
                   permits_acc_inheritance)
qed

lemma accessible_inheritance:
  assumes stat_acc: "Gm of statC accessible_from accC" and
          subclseq: "GdynC C statC" and
       member_dynC: "Gm member_of dynC" and
          dynC_acc: "G(Class dynC) accessible_in (pid accC)"
  shows "Gm of dynC accessible_from accC"
proof -
  from stat_acc
  have member_statC: "Gm member_of statC" 
    by (auto dest: accessible_from_commonD)
  from stat_acc
  show ?thesis
  proof (cases)
    case Immediate
    with member_dynC member_statC subclseq dynC_acc
    show ?thesis
      by (auto intro: accessible_fromR.Immediate permits_acc_inheritance)
  next
    case Overriding
    with member_dynC subclseq dynC_acc
    show ?thesis
      by (auto intro: accessible_fromR.Overriding rtrancl_trancl_trancl)
  qed
qed

subsubsection "fields and methods"


type_synonym
  fspec = "vname × qtname"

translations 
  (type) "fspec" <= (type) "vname × qtname" 

definition
  imethds :: "prog  qtname  (sig,qtname × mhead) tables" where
  "imethds G I =
    iface_rec G I  (λI i ts. (Un_tables ts) ⊕⊕
                        (set_option  table_of (map (λ(s,m). (s,I,m)) (imethods i))))"
text ‹methods of an interface, with overriding and inheritance, cf. 9.2›

definition
  accimethds :: "prog  pname  qtname  (sig,qtname × mhead) tables" where
  "accimethds G pack I =
    (if GIface I accessible_in pack 
     then imethds G I
     else (λ k. {}))"
text ‹only returns imethds if the interface is accessible›

definition
  methd :: "prog  qtname   (sig,qtname × methd) table" where
  "methd G C =
    class_rec G C Map.empty
             (λC c subcls_mthds. 
               filter_tab (λsig m. GC inherits method sig m)
                          subcls_mthds 
               ++ 
               table_of (map (λ(s,m). (s,C,m)) (methods c)))"
text termmethd G C: methods of a class C (statically visible from C), 
     with inheritance and hiding cf. 8.4.6;
     Overriding is captured by dynmethd›.
     Every new method with the same signature coalesces the
     method of a superclass.›

definition
  accmethd :: "prog  qtname  qtname   (sig,qtname × methd) table" where
  "accmethd G S C =
    filter_tab (λsig m. Gmethod sig m of C accessible_from S) (methd G C)"
text termaccmethd G S C: only those methods of termmethd G C, 
        accessible from S›

text ‹Note the class component in the accessibility filter. The class where
    method termm is declared (termdeclC) isn't necessarily accessible 
    from the current scope termS. The method can be made accessible 
    through inheritance, too.
    So we must test accessibility of method termm of class termC 
    (not termdeclclass m)›

definition
  dynmethd :: "prog   qtname  qtname  (sig,qtname × methd) table" where
  "dynmethd G statC dynC =
    (λsig.
       (if GdynC C statC
          then (case methd G statC sig of
                  None  None
                | Some statM 
                     (class_rec G dynC Map.empty
                         (λC c subcls_mthds. 
                            subcls_mthds
                            ++
                            (filter_tab 
                              (λ _ dynM. G,sigdynM overrides statM  dynM=statM)
                              (methd G C) ))
                        ) sig
                )
          else None))"

text termdynmethd G statC dynC: dynamic method lookup of a reference 
        with dynamic class termdynC and static class termstatC
text ‹Note some kind of duality between termmethd and termdynmethd 
        in the termclass_rec arguments. Whereas termmethd filters the 
        subclass methods (to get only the inherited ones), termdynmethd 
        filters the new methods (to get only those methods which actually
        override the methods of the static class)›

definition
  dynimethd :: "prog  qtname  qtname  (sig,qtname × methd) table" where
  "dynimethd G I dynC =
    (λsig. if imethds G I sig  {}
           then methd G dynC sig
           else dynmethd G Object dynC sig)"
text termdynimethd G I dynC: dynamic method lookup of a reference with 
        dynamic class dynC and static interface type I›
text ‹
   When calling an interface method, we must distinguish if the method signature
   was defined in the interface or if it must be an Object method in the other
   case. If it was an interface method we search the class hierarchy
   starting at the dynamic class of the object up to Object to find the 
   first matching method (termmethd). Since all interface methods have 
   public access the method can't be coalesced due to some odd visibility 
   effects like in case of dynmethd. The method will be inherited or 
   overridden in all classes from the first class implementing the interface 
   down to the actual dynamic class.
›

definition
  dynlookup :: "prog   ref_ty  qtname  (sig,qtname × methd) table" where
  "dynlookup G statT dynC =
    (case statT of
      NullT         Map.empty
    | IfaceT I      dynimethd G I      dynC
    | ClassT statC  dynmethd  G statC  dynC
    | ArrayT ty     dynmethd  G Object dynC)"
text termdynlookup G statT dynC: dynamic lookup of a method within the 
    static reference type statT and the dynamic class dynC. 
    In a wellformd context statT will not be NullT and in case
    statT is an array type, dynC=Object›

definition
  fields :: "prog  qtname  ((vname × qtname) × field) list" where
  "fields G C =
    class_rec G C [] (λC c ts. map (λ(n,t). ((n,C),t)) (cfields c) @ ts)"
text termfields G C 
     list of fields of a class, including all the fields of the superclasses
     (private, inherited and hidden ones) not only the accessible ones
     (an instance of a object allocates all these fields›

definition
  accfield :: "prog  qtname  qtname  (vname, qtname  ×  field) table" where
  "accfield G S C =
    (let field_tab = table_of((map (λ((n,d),f).(n,(d,f)))) (fields G C))
      in filter_tab (λn (declC,f). G (declC,fdecl (n,f)) of C accessible_from S)
                    field_tab)"
text  termaccfield G C S: fields of a class termC which are 
         accessible from scope of class
         termS with inheritance and hiding, cf. 8.3›
text ‹note the class component in the accessibility filter (see also 
        termmethd).
   The class declaring field termf (termdeclC) isn't necessarily 
   accessible from scope termS. The field can be made visible through 
   inheritance, too. So we must test accessibility of field termf of class 
   termC (not termdeclclass f)› 

definition
  is_methd :: "prog  qtname   sig  bool"
  where "is_methd G = (λC sig. is_class G C  methd G C sig  None)"

definition
  efname :: "((vname × qtname) × field)  (vname × qtname)"
  where "efname = fst"

lemma efname_simp[simp]:"efname (n,f) = n"
by (simp add: efname_def) 


subsection "imethds"

lemma imethds_rec: "iface G I = Some i; ws_prog G   
  imethds G I = Un_tables ((λJ. imethds  G J)`set (isuperIfs i)) ⊕⊕  
                      (set_option  table_of (map (λ(s,mh). (s,I,mh)) (imethods i)))"
apply (unfold imethds_def)
apply (rule iface_rec [THEN trans])
apply auto
done


(* local lemma *)
lemma imethds_norec:
  "iface G md = Some i; ws_prog G; table_of (imethods i) sig = Some mh   
  (md, mh)  imethds G md sig"
apply (subst imethds_rec)
apply assumption+
apply (rule iffD2)
apply (rule overrides_t_Some_iff)
apply (rule disjI1)
apply (auto elim: table_of_map_SomeI)
done

lemma imethds_declI: "m  imethds G I sig; ws_prog G; is_iface G I  
  (i. iface G (decliface m) = Some i  
  table_of (imethods i) sig = Some (mthd m))   
  (I,decliface m)  (subint1 G)*  m  imethds G (decliface m) sig"
apply (erule rev_mp)
apply (rule ws_subint1_induct, assumption, assumption)
apply (subst imethds_rec, erule conjunct1, assumption)
apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
done

lemma imethds_cases:
  assumes im: "im  imethds G I sig"
    and ifI: "iface G I = Some i"
    and ws: "ws_prog G"
  obtains (NewMethod) "table_of (map (λ(s, mh). (s, I, mh)) (imethods i)) sig = Some im"
    | (InheritedMethod) J where "J  set (isuperIfs i)" and "im  imethds G J sig"
using assms by (auto simp add: imethds_rec)


subsection "accimethd"

lemma accimethds_simp [simp]: 
"GIface I accessible_in pack  accimethds G pack I = imethds G I"
by (simp add: accimethds_def)

lemma accimethdsD:
 "im  accimethds G pack I sig 
   im  imethds G I sig  GIface I accessible_in pack"
by (auto simp add: accimethds_def)

lemma accimethdsI: 
"im  imethds G I sig;GIface I accessible_in pack
  im  accimethds G pack I sig"
by simp

subsection "methd"

lemma methd_rec: "class G C = Some c; ws_prog G   
  methd G C 
    = (if C = Object 
          then Map.empty 
          else filter_tab (λsig m. GC inherits method sig m)
                          (methd G (super c))) 
      ++ table_of (map (λ(s,m). (s,C,m)) (methods c))"
apply (unfold methd_def)
apply (erule class_rec [THEN trans], assumption)
apply (simp)
done

(* local lemma *)
lemma methd_norec: 
 "class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m 
   methd G declC sig = Some (declC, m)"
apply (simp only: methd_rec)
apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
apply (auto elim: table_of_map_SomeI)
done


lemma methd_declC: 
"methd G C sig = Some m; ws_prog G;is_class G C 
 (d. class G (declclass m)=Some d  table_of (methods d) sig=Some (mthd m))  
 GC C (declclass m)  methd G (declclass m) sig = Some m"   
apply (erule rev_mp)
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst methd_rec, assumption)
apply (case_tac "Ca=Object")
apply   (force elim: methd_norec )

apply   simp
apply   (case_tac "table_of (map (λ(s, m). (s, Ca, m)) (methods c)) sig")
apply     (force intro: rtrancl_into_rtrancl2)

apply     (auto intro: methd_norec)
done

lemma methd_inheritedD:
  "class G C = Some c; ws_prog G;methd G C sig = Some m
    (declclass m  C  G C inherits method sig m)"
by (auto simp add: methd_rec)

lemma methd_diff_cls:
"ws_prog G; is_class G C; is_class G D;
 methd G C sig = m; methd G D sig = n; mn
  CD"
by (auto simp add: methd_rec)

lemma method_declared_inI: 
 "table_of (methods c) sig = Some m; class G C = Some c
   Gmdecl (sig,m) declared_in C"
by (auto simp add: cdeclaredmethd_def declared_in_def)

lemma methd_declared_in_declclass: 
 "methd G C sig = Some m; ws_prog G;is_class G C 
  G⊢Methd sig m declared_in (declclass m)"
by (auto dest: methd_declC method_declared_inI)

lemma member_methd:
  assumes member_of: "G⊢Methd sig m member_of C" and
                 ws: "ws_prog G"
  shows "methd G C sig = Some m"
proof -
  from member_of 
  have iscls_C: "is_class G C" 
    by (rule member_of_is_classD)
  from iscls_C ws member_of
  show ?thesis (is "?Methd C")
  proof (induct rule: ws_class_induct')
    case (Object co)
    assume "G ⊢Methd sig m member_of Object"
    then have "G⊢Methd sig m declared_in Object  declclass m = Object"
      by (cases set: members) (cases m, auto dest: subcls1D)
    with ws Object 
    show "?Methd Object"
      by (cases m)
         (auto simp add: declared_in_def cdeclaredmethd_def methd_rec
                  intro:  table_of_mapconst_SomeI)
  next
    case (Subcls C c)
    assume clsC: "class G C = Some c" and
      neq_C_Obj: "C  Object" and
            hyp: "G ⊢Methd sig m member_of super c  ?Methd (super c)" and
      member_of: "G ⊢Methd sig m member_of C"
    from member_of
    show "?Methd C"
    proof (cases)
      case Immediate
      with clsC 
      have "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig = Some m"
        by (cases m)
           (auto simp add: declared_in_def cdeclaredmethd_def
                    intro: table_of_mapconst_SomeI)
      with clsC neq_C_Obj ws 
      show ?thesis
        by (simp add: methd_rec)
    next
      case (Inherited S)
      with clsC
      have  undecl: "Gmid sig undeclared_in C" and
             super: "G ⊢Methd sig m member_of (super c)"
        by (auto dest: subcls1D)
      from clsC undecl 
      have "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig = None"
        by (auto simp add: undeclared_in_def cdeclaredmethd_def
                    intro: table_of_mapconst_NoneI)
      moreover
      from Inherited have "G  C inherits (method sig m)"
        by (auto simp add: inherits_def)
      moreover
      note clsC neq_C_Obj ws super hyp 
      ultimately
      show ?thesis
        by (auto simp add: methd_rec intro: filter_tab_SomeI)
    qed
  qed
qed

(*unused*)
lemma finite_methd:"ws_prog G  finite {methd G C sig |sig C. is_class G C}"
apply (rule finite_is_class [THEN finite_SetCompr2])
apply (intro strip)
apply (erule_tac ws_subcls1_induct, assumption)
apply (subst methd_rec)
apply (assumption)
apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
done

lemma finite_dom_methd:
 "ws_prog G; is_class G C  finite (dom (methd G C))"
apply (erule_tac ws_subcls1_induct)
apply assumption
apply (subst methd_rec)
apply (assumption)
apply (auto intro!: finite_dom_map_of finite_dom_filter_tab)
done


subsection "accmethd"

lemma accmethd_SomeD:
"accmethd G S C sig = Some m
  methd G C sig = Some m  Gmethod sig m of C accessible_from S"
by (auto simp add: accmethd_def)

lemma accmethd_SomeI:
"methd G C sig = Some m; Gmethod sig m of C accessible_from S 
  accmethd G S C sig = Some m"
by (auto simp add: accmethd_def intro: filter_tab_SomeI)

lemma accmethd_declC: 
"accmethd G S C sig = Some m; ws_prog G; is_class G C 
 (d. class G (declclass m)=Some d  
  table_of (methods d) sig=Some (mthd m))  
 GC C (declclass m)  methd G (declclass m) sig = Some m  
 Gmethod sig m of C accessible_from S"
by (auto dest: accmethd_SomeD methd_declC accmethd_SomeI)


lemma finite_dom_accmethd:
 "ws_prog G; is_class G C  finite (dom (accmethd G S C))"
by (auto simp add: accmethd_def intro: finite_dom_filter_tab finite_dom_methd)


subsection "dynmethd"

lemma dynmethd_rec:
"class G dynC = Some c; ws_prog G   
 dynmethd G statC dynC sig
   = (if GdynC C statC
        then (case methd G statC sig of
                None  None
              | Some statM 
                   (case methd G dynC sig of
                        None  dynmethd G statC (super c) sig
                      | Some dynM  
                          (if G,sig dynM overrides statM  dynM = statM 
                              then Some dynM
                              else (dynmethd G statC (super c) sig)
                      )))
         else None)" 
   (is "_  _  ?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig") 
proof -
  assume clsDynC: "class G dynC = Some c" and 
              ws: "ws_prog G"
  then show "?Dynmethd_def dynC sig  = ?Dynmethd_rec dynC c sig" 
  proof (induct rule: ws_class_induct'')
    case (Object co)
    show "?Dynmethd_def Object sig = ?Dynmethd_rec Object co sig"
    proof (cases "GObject C statC") 
      case False
      then show ?thesis by (simp add: dynmethd_def)
    next
      case True
      then have eq_statC_Obj: "statC = Object" ..
      show ?thesis 
      proof (cases "methd G statC sig")
        case None then show ?thesis by (simp add: dynmethd_def)
      next
        case Some
        with True Object ws eq_statC_Obj 
        show ?thesis
          by (auto simp add: dynmethd_def class_rec
                      intro: filter_tab_SomeI)
      qed
    qed
  next  
    case (Subcls dynC c sc)
    show "?Dynmethd_def dynC sig = ?Dynmethd_rec dynC c sig"
    proof (cases "GdynC C statC") 
      case False
      then show ?thesis by (simp add: dynmethd_def)
    next
      case True
      note subclseq_dynC_statC = True
      show ?thesis
      proof (cases "methd G statC sig")
        case None then show ?thesis by (simp add: dynmethd_def)
      next
        case (Some statM)
        note statM = Some
        let ?filter = 
              "λC. filter_tab
                (λ_ dynM. G,sig  dynM overrides statM  dynM = statM)
                (methd G C)"
        let ?class_rec =
              "λC. class_rec G C Map.empty
                           (λC c subcls_mthds. subcls_mthds ++ (?filter C))"
        from statM Subcls ws subclseq_dynC_statC
        have dynmethd_dynC_def:
             "?Dynmethd_def dynC sig =
                ((?class_rec (super c)) 
                 ++
                (?filter dynC)) sig"
         by (simp (no_asm_simp) only: dynmethd_def class_rec)
            auto
       show ?thesis
       proof (cases "dynC = statC")
         case True
         with subclseq_dynC_statC statM dynmethd_dynC_def
         have "?Dynmethd_def dynC sig = Some statM"
           by (auto intro: map_add_find_right filter_tab_SomeI)
         with subclseq_dynC_statC True Some 
         show ?thesis
           by auto
       next
         case False
         with subclseq_dynC_statC Subcls 
         have subclseq_super_statC: "G(super c) C statC"
           by (blast dest: subclseq_superD)
         show ?thesis
         proof (cases "methd G dynC sig") 
           case None
           then have "?filter dynC sig = None"
             by (rule filter_tab_None)
           then have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
             by (simp add: dynmethd_dynC_def)
           with  subclseq_super_statC statM None
           have "?Dynmethd_def dynC sig = ?Dynmethd_def (super c) sig"
             by (auto simp add: empty_def dynmethd_def)
           with None subclseq_dynC_statC statM
           show ?thesis 
             by simp
         next
           case (Some dynM)
           note dynM = Some
           let ?Termination = "G  qmdecl sig dynM overrides qmdecl sig statM 
                               dynM = statM"
           show ?thesis
           proof (cases "?filter dynC sig")
             case None
             with dynM 
             have no_termination: "¬ ?Termination"
               by (simp add: filter_tab_def)
             from None 
             have "?Dynmethd_def dynC sig=?class_rec (super c) sig"
               by (simp add: dynmethd_dynC_def)
             with subclseq_super_statC statM dynM no_termination
             show ?thesis
               by (auto simp add: empty_def dynmethd_def)
           next
             case Some
             with dynM
             have "termination": "?Termination"
               by (auto)
             with Some dynM
             have "?Dynmethd_def dynC sig=Some dynM"
              by (auto simp add: dynmethd_dynC_def)
             with subclseq_super_statC statM dynM "termination"
             show ?thesis
               by (auto simp add: dynmethd_def)
           qed
         qed
       qed
     qed
   qed
 qed
qed
               
lemma dynmethd_C_C:"is_class G C; ws_prog G 
 dynmethd G C C sig = methd G C sig"          
apply (auto simp add: dynmethd_rec)
done
 
lemma dynmethdSomeD: 
 "dynmethd G statC dynC sig = Some dynM; is_class G dynC; ws_prog G 
   GdynC C statC  ( statM. methd G statC sig = Some statM)"
by (auto simp add: dynmethd_rec)
 
lemma dynmethd_Some_cases:
  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
    and is_cls_dynC: "is_class G dynC"
    and ws: "ws_prog G"
  obtains (Static) "methd G statC sig = Some dynM"
    | (Overrides) statM
      where "methd G statC sig = Some statM"
        and "dynM  statM"
        and "G,sigdynM overrides statM"
proof -
  from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
  from clsDynC ws dynM Static Overrides
  show ?thesis
  proof (induct rule: ws_class_induct)
    case (Object co)
    with ws  have "statC = Object" 
      by (auto simp add: dynmethd_rec)
    with ws Object show ?thesis by (auto simp add: dynmethd_C_C)
  next
    case (Subcls C c)
    with ws show ?thesis
      by (auto simp add: dynmethd_rec)
  qed
qed

lemma no_override_in_Object:
  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
            is_cls_dynC: "is_class G dynC" and
                     ws: "ws_prog G" and
                  statM: "methd G statC sig = Some statM" and
         neq_dynM_statM: "dynMstatM"
  shows "dynC  Object"
proof -
  from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
  from clsDynC ws dynM statM neq_dynM_statM 
  show ?thesis (is "?P dynC")
  proof (induct rule: ws_class_induct)
    case (Object co)
    with ws  have "statC = Object" 
      by (auto simp add: dynmethd_rec)
    with ws Object show "?P Object" by (auto simp add: dynmethd_C_C)
  next
    case (Subcls dynC c)
    with ws show "?P dynC"
      by (auto simp add: dynmethd_rec)
  qed
qed


lemma dynmethd_Some_rec_cases:
  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
    and clsDynC: "class G dynC = Some c"
    and ws: "ws_prog G"
  obtains (Static) "methd G statC sig = Some dynM"
    | (Override) statM where "methd G statC sig = Some statM"
        and "methd G dynC sig = Some dynM" and "statM  dynM"
        and "G,sig dynM overrides statM"
    | (Recursion) "dynC  Object" and "dynmethd G statC (super c) sig = Some dynM"
proof -
  from clsDynC have *: "is_class G dynC" by simp
  from ws clsDynC dynM Static Override Recursion
  show ?thesis
    by (auto simp add: dynmethd_rec dest: no_override_in_Object [OF dynM * ws])
qed

lemma dynmethd_declC: 
"dynmethd G statC dynC sig = Some m;
  is_class G statC;ws_prog G
  
  (d. class G (declclass m)=Some d  table_of (methods d) sig=Some (mthd m)) 
  GdynC C (declclass m)  methd G (declclass m) sig = Some m"
proof - 
  assume  is_cls_statC: "is_class G statC" 
  assume            ws: "ws_prog G"  
  assume             m: "dynmethd G statC dynC sig = Some m"
  from m 
  have "GdynC C statC" by (auto simp add: dynmethd_def)
  from this is_cls_statC 
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  from is_cls_dynC ws m  
  show ?thesis (is "?P dynC") 
  proof (induct rule: ws_class_induct')
    case (Object co)
    with ws have "statC=Object" by (auto simp add: dynmethd_rec)
    with ws Object  
    show "?P Object" 
      by (auto simp add: dynmethd_C_C dest: methd_declC)
  next
    case (Subcls dynC c)
    assume   hyp: "dynmethd G statC (super c) sig = Some m  ?P (super c)" and
         clsDynC: "class G dynC = Some c"  and
              m': "dynmethd G statC dynC sig = Some m" and
    neq_dynC_Obj: "dynC  Object"
    from ws this obtain statM where
      subclseq_dynC_statC: "GdynC C statC" and 
                     statM: "methd G statC sig = Some statM"
      by (blast dest: dynmethdSomeD)
    from clsDynC neq_dynC_Obj 
    have subclseq_dynC_super: "GdynC C (super c)" 
      by (auto intro: subcls1I) 
    from m' clsDynC ws 
    show "?P dynC"
    proof (cases rule: dynmethd_Some_rec_cases) 
      case Static
      with is_cls_statC ws subclseq_dynC_statC 
      show ?thesis 
        by (auto intro: rtrancl_trans dest: methd_declC)
    next
      case Override
      with clsDynC ws 
      show ?thesis 
        by (auto dest: methd_declC)
    next
      case Recursion
      with hyp subclseq_dynC_super 
      show ?thesis 
        by (auto intro: rtrancl_trans) 
    qed
  qed
qed

lemma methd_Some_dynmethd_Some:
  assumes     statM: "methd G statC sig = Some statM" and
           subclseq: "GdynC C statC" and
       is_cls_statC: "is_class G statC" and
                 ws: "ws_prog G"
  shows " dynM. dynmethd G statC dynC sig = Some dynM"
    (is "?P dynC")
proof -
  from subclseq is_cls_statC 
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  then obtain dc where
    clsDynC: "class G dynC = Some dc" by blast
  from clsDynC ws subclseq 
  show "?thesis"
  proof (induct rule: ws_class_induct)
    case (Object co)
    with ws  have "statC = Object" 
      by (auto)
    with ws Object statM
    show "?P Object"  
      by (auto simp add: dynmethd_C_C)
  next
    case (Subcls dynC dc)
    assume clsDynC': "class G dynC = Some dc"
    assume neq_dynC_Obj: "dynC  Object"
    assume hyp: "Gsuper dcC statC  ?P (super dc)"
    assume subclseq': "GdynCC statC"
    then
    show "?P dynC"
    proof (cases rule: subclseq_cases)
      case Eq
      with ws statM clsDynC' 
      show ?thesis
        by (auto simp add: dynmethd_rec)
    next
      case Subcls
      assume "GdynCC statC"
      from this clsDynC' 
      have "Gsuper dcC statC" by (rule subcls_superD)
      with hyp ws clsDynC' subclseq' statM
      show ?thesis
        by (auto simp add: dynmethd_rec)
    qed
  qed
qed

lemma dynmethd_cases:
  assumes statM: "methd G statC sig = Some statM"
    and subclseq: "GdynC C statC"
    and is_cls_statC: "is_class G statC"
    and ws: "ws_prog G"
  obtains (Static) "dynmethd G statC dynC sig = Some statM"
    | (Overrides) dynM where "dynmethd G statC dynC sig = Some dynM"
        and "dynM  statM" and "G,sigdynM overrides statM"
proof -
  note hyp_static = Static and hyp_override = Overrides
  from subclseq is_cls_statC 
  have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
  then obtain dc where
    clsDynC: "class G dynC = Some dc" by blast
  from statM subclseq is_cls_statC ws 
  obtain dynM where dynM: "dynmethd G statC dynC sig = Some dynM"
    by (blast dest: methd_Some_dynmethd_Some)
  from dynM is_cls_dynC ws 
  show ?thesis
  proof (cases rule: dynmethd_Some_cases)
    case Static
    with hyp_static dynM statM show ?thesis by simp
  next
    case Overrides
    with hyp_override dynM statM show ?thesis by simp
  qed
qed

lemma ws_dynmethd:
  assumes  statM: "methd G statC sig = Some statM" and
        subclseq: "GdynC C statC" and
    is_cls_statC: "is_class G statC" and
              ws: "ws_prog G"
  shows
    " dynM. dynmethd G statC dynC sig = Some dynM 
             is_static dynM = is_static statM  GresTy dynMresTy statM"
proof - 
  from statM subclseq is_cls_statC ws
  show ?thesis
  proof (cases rule: dynmethd_cases)
    case Static
    with statM 
    show ?thesis
      by simp
  next
    case Overrides
    with ws
    show ?thesis
      by (auto dest: ws_overrides_commonD)
  qed
qed

subsection "dynlookup"

lemma dynlookup_cases:
  assumes "dynlookup G statT dynC sig = x"
  obtains (NullT) "statT = NullT" and "Map.empty sig = x"
    | (IfaceT) I where "statT = IfaceT I" and "dynimethd G I dynC sig = x"
    | (ClassT) statC where "statT = ClassT statC" and "dynmethd G statC dynC sig = x"
    | (ArrayT) ty where "statT = ArrayT ty" and "dynmethd G Object dynC sig = x"
using assms by (cases statT) (auto simp add: dynlookup_def)

subsection "fields"

lemma fields_rec: "class G C = Some c; ws_prog G   
  fields G C = map (λ(fn,ft). ((fn,C),ft)) (cfields c) @  
  (if C = Object then [] else fields G (super c))"
apply (simp only: fields_def)
apply (erule class_rec [THEN trans])
apply assumption
apply clarsimp
done

(* local lemma *)
lemma fields_norec: 
"class G fd = Some c; ws_prog G;  table_of (cfields c) fn = Some f 
  table_of (fields G fd) (fn,fd) = Some f"
apply (subst fields_rec)
apply assumption+
apply (subst map_of_append)
apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
apply (auto elim: table_of_map2_SomeI)
done

(* local lemma *)
lemma table_of_fieldsD:
"table_of (map (λ(fn,ft). ((fn,C),ft)) (cfields c)) efn = Some f
 (declclassf efn) = C  table_of (cfields c) (fname efn) = Some f"
apply (case_tac "efn")
by auto

lemma fields_declC: 
 "table_of (fields G C) efn = Some f; ws_prog G; is_class G C   
  (d. class G (declclassf efn) = Some d  
                    table_of (cfields d) (fname efn)=Some f)  
  GC C (declclassf efn)   table_of (fields G (declclassf efn)) efn = Some f"
apply (erule rev_mp)
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst fields_rec, assumption)
apply clarify
apply (simp only: map_of_append)
apply (case_tac "table_of (map (case_prod (λfn. Pair (fn, Ca))) (cfields c)) efn") 
apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)

apply   (frule_tac fd="Ca" in fields_norec)
apply     assumption
apply     blast
apply   (frule table_of_fieldsD)  
apply   (frule_tac n="table_of (map (case_prod (λfn. Pair (fn, Ca))) (cfields c))"
              and  m="table_of (if Ca = Object then [] else fields G (super c))"
         in map_add_find_right)
apply   (case_tac "efn")
apply   (simp)
done

lemma fields_emptyI: "y. ws_prog G; class G C = Some c;cfields c = [];  
  C  Object  class G (super c) = Some y  fields G (super c) = []   
  fields G C = []"
apply (subst fields_rec)
apply assumption
apply auto
done

(* easier than with table_of *)
lemma fields_mono_lemma: 
"x  set (fields G C); GD C C; ws_prog G 
  x  set (fields G D)"
apply (erule rev_mp)
apply (erule converse_rtrancl_induct)
apply  fast
apply (drule subcls1D)
apply clarsimp
apply (subst fields_rec)
apply   auto
done


lemma ws_unique_fields_lemma: 
 "(efn,fd)   set (fields G (super c)); fc  set (cfields c); ws_prog G;  
   fname efn = fname fc; declclassf efn = C;
   class G C = Some c; C  Object; class G (super c) = Some d  R"
apply (frule_tac ws_prog_cdeclD [THEN conjunct2], assumption, assumption)
apply (drule_tac weak_map_of_SomeI)
apply (frule_tac subcls1I [THEN subcls1_irrefl], assumption, assumption)
apply (auto dest: fields_declC [THEN conjunct2 [THEN conjunct1[THEN rtranclD]]])
done

lemma ws_unique_fields: "is_class G C; ws_prog G; 
       C c. class G C = Some c  unique (cfields c)  
      unique (fields G C)" 
apply (rule ws_subcls1_induct, assumption, assumption)
apply (subst fields_rec, assumption)            
apply (auto intro!: unique_map_inj inj_onI 
            elim!: unique_append ws_unique_fields_lemma fields_norec)
done


subsection "accfield"

lemma accfield_fields: 
 "accfield G S C fn = Some f 
   table_of (fields G C) (fn, declclass f) = Some (fld f)"
apply (simp only: accfield_def Let_def)
apply (rule table_of_remap_SomeD)
apply auto
done


lemma accfield_declC_is_class: 
 "is_class G C; accfield G S C en = Some (fd, f); ws_prog G   
   is_class G fd"
apply (drule accfield_fields)
apply (drule fields_declC [THEN conjunct1], assumption)
apply auto
done

lemma accfield_accessibleD: 
  "accfield G S C fn = Some f  G⊢Field fn f of C accessible_from S"
by (auto simp add: accfield_def Let_def)

subsection "is methd"

lemma is_methdI: 
"class G C = Some y; methd G C sig = Some b  is_methd G C sig"
apply (unfold is_methd_def)
apply auto
done

lemma is_methdD: 
"is_methd G C sig  class G C  None  methd G C sig  None"
apply (unfold is_methd_def)
apply auto
done

lemma finite_is_methd: 
 "ws_prog G  finite (Collect (case_prod (is_methd G)))"
apply (unfold is_methd_def)
apply (subst Collect_case_prod_Sigma)
apply (rule finite_is_class [THEN finite_SigmaI])
apply (simp only: mem_Collect_eq)
apply (fold dom_def)
apply (erule finite_dom_methd)
apply assumption
done

subsubsection "calculation of the superclasses of a class"

definition
  superclasses :: "prog  qtname  qtname set" where
 "superclasses G C = class_rec G C {} 
                       (λ C c superclss. (if C=Object 
                                            then {} 
                                            else insert (super c) superclss))"
   
lemma superclasses_rec: "class G C = Some c; ws_prog G   
 superclasses G C 
 = (if (C=Object) 
       then {}
       else insert (super c) (superclasses G (super c)))"
apply (unfold superclasses_def)
apply (erule class_rec [THEN trans], assumption)
apply (simp)
done

lemma superclasses_mono:
  assumes clsrel: "GCC D"
  and ws: "ws_prog G"
  and cls_C: "class G C = Some c"
  and wf: "C c. class G C = Some c; C  Object
     sc. class G (super c) = Some sc"
  and x: "xsuperclasses G D"
  shows "xsuperclasses G C" using clsrel cls_C x
proof (induct arbitrary: c rule: converse_trancl_induct)
  case (base C)
  with wf ws show ?case
    by (auto    intro: no_subcls1_Object 
             simp add: superclasses_rec subcls1_def)
next
  case (step C S)
  moreover note wf ws
  moreover from calculation 
  have "xsuperclasses G S"
    by (force intro: no_subcls1_Object simp add: subcls1_def)
  moreover from calculation 
  have "super c = S" 
    by (auto intro: no_subcls1_Object simp add: subcls1_def)
  ultimately show ?case 
    by (auto intro: no_subcls1_Object simp add: superclasses_rec)
qed

lemma subclsEval:
  assumes clsrel: "GCC D"
  and ws: "ws_prog G"
  and cls_C: "class G C = Some c"
  and wf: "C c. class G C = Some c; C  Object
     sc. class G (super c) = Some sc"
  shows "Dsuperclasses G C" using clsrel cls_C
proof (induct arbitrary: c rule: converse_trancl_induct)
  case (base C)
  with ws wf show ?case
    by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
next
  case (step C S)
  with ws wf show ?case
    by - (rule superclasses_mono,
          auto dest: no_subcls1_Object simp add: subcls1_def )
qed

end