Theory WellForm

(*  Title:      HOL/Bali/WellForm.thy
    Author:     David von Oheimb and Norbert Schirmer
*)

subsection ‹Well-formedness of Java programs›
theory WellForm imports DefiniteAssignment begin

text ‹
For static checks on expressions and statements, see WellType.thy

improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
\begin{itemize}
\item a method implementing or overwriting another method may have a result 
      type that widens to the result type of the other method 
      (instead of identical type)
\item if a method hides another method (both methods have to be static!)
  there are no restrictions to the result type 
  since the methods have to be static and there is no dynamic binding of 
  static methods
\item if an interface inherits more than one method with the same signature, the
  methods need not have identical return types
\end{itemize}
simplifications:
\begin{itemize}
\item Object and standard exceptions are assumed to be declared like normal 
      classes
\end{itemize}
›

subsubsection "well-formed field declarations"
text  ‹well-formed field declaration (common part for classes and interfaces),
        cf. 8.3 and (9.3)›

definition
  wf_fdecl :: "prog  pname  fdecl  bool"
  where "wf_fdecl G P = (λ(fn,f). is_acc_type G P (type f))"

lemma wf_fdecl_def2: "fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
apply (unfold wf_fdecl_def)
apply simp
done



subsubsection "well-formed method declarations"
  (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
  (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)

text ‹
A method head is wellformed if:
\begin{itemize}
\item the signature and the method head agree in the number of parameters
\item all types of the parameters are visible
\item the result type is visible
\item the parameter names are unique
\end{itemize} 
›
definition
  wf_mhead :: "prog  pname  sig  mhead  bool" where
  "wf_mhead G P = (λ sig mh. length (parTs sig) = length (pars mh) 
                            ( Tset (parTs sig). is_acc_type G P T)  
                            is_acc_type G P (resTy mh) 
                            distinct (pars mh))"


text ‹
A method declaration is wellformed if:
\begin{itemize}
\item the method head is wellformed
\item the names of the local variables are unique
\item the types of the local variables must be accessible
\item the local variables don't shadow the parameters
\item the class of the method is defined
\item the body statement is welltyped with respect to the
      modified environment of local names, were the local variables, 
      the parameters the special result variable (Res) and This are assoziated
      with there types. 
\end{itemize}
›

definition
  callee_lcl :: "qtname  sig  methd  lenv" where
  "callee_lcl C sig m =
    (λk. (case k of
            EName e 
             (case e of 
                  VNam v 
                  ((table_of (lcls (mbody m)))(pars m [↦] parTs sig)) v
                | Res  Some (resTy m))
          | This  if is_static m then None else Some (Class C)))"

definition
  parameters :: "methd  lname set" where
  "parameters m = set (map (EName  VNam) (pars m))  (if (static m) then {} else {This})"

definition
  wf_mdecl :: "prog  qtname  mdecl  bool" where
  "wf_mdecl G C =
      (λ(sig,m).
          wf_mhead G (pid C) sig (mhead m)  
          unique (lcls (mbody m))  
          ((vn,T)set (lcls (mbody m)). is_acc_type G (pid C) T)  
          (pnset (pars m). table_of (lcls (mbody m)) pn = None) 
          jumpNestingOkS {Ret} (stmt (mbody m))  
          is_class G C 
          prg=G,cls=C,lcl=callee_lcl C sig m(stmt (mbody m))∷√ 
          ( A. prg=G,cls=C,lcl=callee_lcl C sig m 
                 parameters m »stmt (mbody m)» A 
                Result  nrm A))"

lemma callee_lcl_VNam_simp [simp]:
"callee_lcl C sig m (EName (VNam v)) 
  = ((table_of (lcls (mbody m)))(pars m [↦] parTs sig)) v"
by (simp add: callee_lcl_def)
 
lemma callee_lcl_Res_simp [simp]:
"callee_lcl C sig m (EName Res) = Some (resTy m)" 
by (simp add: callee_lcl_def)

lemma callee_lcl_This_simp [simp]:
"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))" 
by (simp add: callee_lcl_def)

lemma callee_lcl_This_static_simp:
"is_static m  callee_lcl C sig m (This) = None"
by simp

lemma callee_lcl_This_not_static_simp:
"¬ is_static m  callee_lcl C sig m (This) = Some (Class C)"
by simp

lemma wf_mheadI: 
"length (parTs sig) = length (pars m); Tset (parTs sig). is_acc_type G P T;
  is_acc_type G P (resTy m); distinct (pars m)   
  wf_mhead G P sig m"
apply (unfold wf_mhead_def)
apply (simp (no_asm_simp))
done

lemma wf_mdeclI: "  
  wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
  (pnset (pars m). table_of (lcls (mbody m)) pn = None); 
  (vn,T)set (lcls (mbody m)). is_acc_type G (pid C) T;
  jumpNestingOkS {Ret} (stmt (mbody m));
  is_class G C;
  prg=G,cls=C,lcl=callee_lcl C sig m(stmt (mbody m))∷√;
  ( A. prg=G,cls=C,lcl=callee_lcl C sig m  parameters m »stmt (mbody m)» A
         Result  nrm A)
     
  wf_mdecl G C (sig,m)"
apply (unfold wf_mdecl_def)
apply simp
done

lemma wf_mdeclE [consumes 1]:  
  "wf_mdecl G C (sig,m); 
    wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
     pnset (pars m). table_of (lcls (mbody m)) pn = None; 
     (vn,T)set (lcls (mbody m)). is_acc_type G (pid C) T;
     jumpNestingOkS {Ret} (stmt (mbody m));
     is_class G C;
     prg=G,cls=C,lcl=callee_lcl C sig m(stmt (mbody m))∷√;
   ( A. prg=G,cls=C,lcl=callee_lcl C sig m parameters m »stmt (mbody m)» A
         Result  nrm A)
      P
    P"
by (unfold wf_mdecl_def) simp


lemma wf_mdeclD1: 
"wf_mdecl G C (sig,m)   
   wf_mhead G (pid C) sig (mhead m)  unique (lcls (mbody m))   
  (pnset (pars m). table_of (lcls (mbody m)) pn = None)  
  ((vn,T)set (lcls (mbody m)). is_acc_type G (pid C) T)"
apply (unfold wf_mdecl_def)
apply simp
done

lemma wf_mdecl_bodyD: 
"wf_mdecl G C (sig,m)   
 (T. prg=G,cls=C,lcl=callee_lcl C sig mBody C (stmt (mbody m))∷-T  
      GT(resTy m))"
apply (unfold wf_mdecl_def)
apply clarify
apply (rule_tac x="(resTy m)" in exI)
apply (unfold wf_mhead_def)
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
done


(*
lemma static_Object_methodsE [elim!]: 
 "⟦wf_mdecl G Object (sig, m);static m⟧ ⟹ R"
apply (unfold wf_mdecl_def)
apply auto
done
*)

lemma rT_is_acc_type: 
  "wf_mhead G P sig m  is_acc_type G P (resTy m)"
apply (unfold wf_mhead_def)
apply auto
done

subsubsection "well-formed interface declarations"
  (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)

text ‹
A interface declaration is wellformed if:
\begin{itemize}
\item the interface hierarchy is wellstructured
\item there is no class with the same name
\item the method heads are wellformed and not static and have Public access
\item the methods are uniquely named
\item all superinterfaces are accessible
\item the result type of a method overriding a method of Object widens to the
      result type of the overridden method.
      Shadowing static methods is forbidden.
\item the result type of a method overriding a set of methods defined in the
      superinterfaces widens to each of the corresponding result types
\end{itemize}
›
definition
  wf_idecl :: "prog   idecl  bool" where
 "wf_idecl G =
    (λ(I,i). 
        ws_idecl G I (isuperIfs i)  
        ¬is_class G I 
        ((sig,mh)set (imethods i). wf_mhead G (pid I) sig mh  
                                     ¬is_static mh 
                                      accmodi mh = Public) 
        unique (imethods i) 
        ( Jset (isuperIfs i). is_acc_iface G (pid I) J) 
        (table_of (imethods i)
          hiding (methd G Object)
          under  (λ new old. accmodi old  Private)
          entails (λnew old. GresTy newresTy old  
                             is_static new = is_static old))  
        (set_option  table_of (imethods i) 
               hidings Un_tables((λJ.(imethds G J))`set (isuperIfs i))
               entails (λnew old. GresTy newresTy old)))"

lemma wf_idecl_mhead: "wf_idecl G (I,i); (sig,mh)set (imethods i)   
  wf_mhead G (pid I) sig mh  ¬is_static mh  accmodi mh = Public"
apply (unfold wf_idecl_def)
apply auto
done

lemma wf_idecl_hidings: 
"wf_idecl G (I, i)  
  (λs. set_option (table_of (imethods i) s)) 
  hidings Un_tables ((λJ. imethds G J) ` set (isuperIfs i))  
  entails λnew old. GresTy newresTy old"
apply (unfold wf_idecl_def o_def)
apply simp
done

lemma wf_idecl_hiding:
"wf_idecl G (I, i)  
 (table_of (imethods i)
           hiding (methd G Object)
           under  (λ new old. accmodi old  Private)
           entails (λnew old. GresTy newresTy old  
                              is_static new = is_static old))"
apply (unfold wf_idecl_def)
apply simp
done

lemma wf_idecl_supD: 
"wf_idecl G (I,i); J  set (isuperIfs i) 
  is_acc_iface G (pid I) J  (J, I)  (subint1 G)+"
apply (unfold wf_idecl_def ws_idecl_def)
apply auto
done

subsubsection "well-formed class declarations"
  (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
   class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)

text ‹
A class declaration is wellformed if:
\begin{itemize}
\item there is no interface with the same name
\item all superinterfaces are accessible and for all methods implementing 
      an interface method the result type widens to the result type of 
      the interface method, the method is not static and offers at least 
      as much access 
      (this actually means that the method has Public access, since all 
      interface methods have public access)
\item all field declarations are wellformed and the field names are unique
\item all method declarations are wellformed and the method names are unique
\item the initialization statement is welltyped
\item the classhierarchy is wellstructured
\item Unless the class is Object:
      \begin{itemize}
      \item the superclass is accessible
      \item for all methods overriding another method (of a superclass )the
            result type widens to the result type of the overridden method,
            the access modifier of the new method provides at least as much
            access as the overwritten one.
      \item for all methods hiding a method (of a superclass) the hidden 
            method must be static and offer at least as much access rights.
            Remark: In contrast to the Java Language Specification we don't
            restrict the result types of the method
            (as in case of overriding), because there seems to be no reason,
            since there is no dynamic binding of static methods.
            (cf. 8.4.6.3 vs. 15.12.1).
            Stricly speaking the restrictions on the access rights aren't 
            necessary to, since the static type and the access rights 
            together determine which method is to be called statically. 
            But if a class gains more then one static method with the 
            same signature due to inheritance, it is confusing when the 
            method selection depends on the access rights only: 
            e.g.
              Class C declares static public method foo().
              Class D is subclass of C and declares static method foo()
              with default package access.
              D.foo() ? if this call is in the same package as D then
                        foo of class D is called, otherwise foo of class C.
      \end{itemize}

\end{itemize}
›
(* to Table *)
definition
  entails :: "('a,'b) table  ('b  bool)  bool" ("_ entails _" 20)
  where "(t entails P) = (k.  x  t k: P x)"

lemma entailsD:
 "t entails P; t k = Some x  P x"
by (simp add: entails_def)

lemma empty_entails[simp]: "Map.empty entails P"
by (simp add: entails_def)

definition
  wf_cdecl :: "prog  cdecl  bool" where
  "wf_cdecl G =
     (λ(C,c).
      ¬is_iface G C 
      (Iset (superIfs c). is_acc_iface G (pid C) I 
        (s.  im  imethds G I s.
            ( cm  methd  G C s: GresTy cmresTy im 
                                     ¬ is_static cm 
                                     accmodi im  accmodi cm))) 
      (fset (cfields c). wf_fdecl G (pid C) f)  unique (cfields c)  
      (mset (methods c). wf_mdecl G C m)  unique (methods c) 
      jumpNestingOkS {} (init c) 
      ( A. prg=G,cls=C,lcl=Map.empty {} »init c» A) 
      prg=G,cls=C,lcl=Map.empty(init c)∷√  ws_cdecl G C (super c) 
      (C  Object  
            (is_acc_class G (pid C) (super c) 
            (table_of (map (λ (s,m). (s,C,m)) (methods c)) 
             entails (λ new.  old sig. 
                       (G,signew overridesS old 
                         (GresTy newresTy old 
                             accmodi old  accmodi new 
                             ¬is_static old)) 
                       (G,signew hides old 
                          (accmodi old  accmodi new 
                              is_static old)))) 
            )))"

(*
definition wf_cdecl :: "prog ⇒ cdecl ⇒ bool" where
"wf_cdecl G ≡ 
   λ(C,c).
      ¬is_iface G C ∧
      (∀I∈set (superIfs c). is_acc_iface G (pid C) I ∧
        (∀s. ∀ im ∈ imethds G I s.
            (∃ cm ∈ methd  G C s: G⊢resTy (mthd cm)≼resTy (mthd im) ∧
                                     ¬ is_static cm ∧
                                     accmodi im ≤ accmodi cm))) ∧
      (∀f∈set (cfields c). wf_fdecl G (pid C) f) ∧ unique (cfields c) ∧ 
      (∀m∈set (methods c). wf_mdecl G C m) ∧ unique (methods c) ∧ 
      ⦇prg=G,cls=C,lcl=empty⦈⊢(init c)∷√ ∧ ws_cdecl G C (super c) ∧
      (C ≠ Object ⟶ 
            (is_acc_class G (pid C) (super c) ∧
            (table_of (map (λ (s,m). (s,C,m)) (methods c)) 
              hiding methd G (super c)
              under (λ new old. G⊢new overrides old)
              entails (λ new old. 
                           (G⊢resTy (mthd new)≼resTy (mthd old) ∧
                            accmodi old ≤ accmodi new ∧
                           ¬ is_static old)))  ∧
            (table_of (map (λ (s,m). (s,C,m)) (methods c)) 
              hiding methd G (super c)
              under (λ new old. G⊢new hides old)
              entails (λ new old. is_static old ∧ 
                                  accmodi old ≤ accmodi new))  ∧
            (table_of (cfields c) hiding accfield G C (super c)
              entails (λ newF oldF. accmodi oldF ≤ access newF))))"
*)

lemma wf_cdeclE [consumes 1]: 
 "wf_cdecl G (C,c);
   ¬is_iface G C;
    (Iset (superIfs c). is_acc_iface G (pid C) I 
        (s.  im  imethds G I s.
            ( cm  methd  G C s: GresTy cmresTy im 
                                     ¬ is_static cm 
                                     accmodi im  accmodi cm))); 
      fset (cfields c). wf_fdecl G (pid C) f; unique (cfields c); 
      mset (methods c). wf_mdecl G C m; unique (methods c);
      jumpNestingOkS {} (init c);
       A. prg=G,cls=C,lcl=Map.empty {} »init c» A;
      prg=G,cls=C,lcl=Map.empty(init c)∷√; 
      ws_cdecl G C (super c); 
      (C  Object  
            (is_acc_class G (pid C) (super c) 
            (table_of (map (λ (s,m). (s,C,m)) (methods c)) 
             entails (λ new.  old sig. 
                       (G,signew overridesS old 
                         (GresTy newresTy old 
                             accmodi old  accmodi new 
                             ¬is_static old)) 
                       (G,signew hides old 
                          (accmodi old  accmodi new 
                              is_static old)))) 
            ))  P
    P"
by (unfold wf_cdecl_def) simp

lemma wf_cdecl_unique: 
"wf_cdecl G (C,c)  unique (cfields c)  unique (methods c)"
apply (unfold wf_cdecl_def)
apply auto
done

lemma wf_cdecl_fdecl: 
"wf_cdecl G (C,c); fset (cfields c)  wf_fdecl G (pid C) f"
apply (unfold wf_cdecl_def)
apply auto
done

lemma wf_cdecl_mdecl: 
"wf_cdecl G (C,c); mset (methods c)  wf_mdecl G C m"
apply (unfold wf_cdecl_def)
apply auto
done

lemma wf_cdecl_impD: 
"wf_cdecl G (C,c); Iset (superIfs c) 
 is_acc_iface G (pid C) I   
    (s. im  imethds G I s.  
        (cm  methd G C s: GresTy cmresTy im  ¬is_static cm 
                                   accmodi im  accmodi cm))"
apply (unfold wf_cdecl_def)
apply auto
done

lemma wf_cdecl_supD: 
"wf_cdecl G (C,c); C  Object   
  is_acc_class G (pid C) (super c)  (super c,C)  (subcls1 G)+  
   (table_of (map (λ (s,m). (s,C,m)) (methods c)) 
    entails (λ new.  old sig. 
                 (G,signew overridesS old 
                   (GresTy newresTy old 
                       accmodi old  accmodi new 
                       ¬is_static old)) 
                 (G,signew hides old 
                    (accmodi old  accmodi new 
                        is_static old))))"
apply (unfold wf_cdecl_def ws_cdecl_def)
apply auto
done


lemma wf_cdecl_overrides_SomeD:
"wf_cdecl G (C,c); C  Object; table_of (methods c) sig = Some newM;
  G,sig(C,newM) overridesS old
   GresTy newMresTy old 
       accmodi old  accmodi newM 
       ¬ is_static old" 
apply (drule (1) wf_cdecl_supD)
apply (clarify)
apply (drule entailsD)
apply   (blast intro: table_of_map_SomeI)
apply (drule_tac x="old" in spec)
apply (auto dest: overrides_eq_sigD simp add: msig_def)
done

lemma wf_cdecl_hides_SomeD:
"wf_cdecl G (C,c); C  Object; table_of (methods c) sig = Some newM;
  G,sig(C,newM) hides old
   accmodi old  access newM 
       is_static old" 
apply (drule (1) wf_cdecl_supD)
apply (clarify)
apply (drule entailsD)
apply   (blast intro: table_of_map_SomeI)
apply (drule_tac x="old" in spec)
apply (auto dest: hides_eq_sigD simp add: msig_def)
done

lemma wf_cdecl_wt_init: 
 "wf_cdecl G (C, c)  prg=G,cls=C,lcl=Map.emptyinit c∷√"
apply (unfold wf_cdecl_def)
apply auto
done


subsubsection "well-formed programs"
  (* well-formed program, cf. 8.1, 9.1 *)

text ‹
A program declaration is wellformed if:
\begin{itemize}
\item the class ObjectC of Object is defined
\item every method of Object has an access modifier distinct from Package. 
      This is
      necessary since every interface automatically inherits from Object.  
      We must know, that every time a Object method is "overriden" by an 
      interface method this is also overriden by the class implementing the
      the interface (see implement_dynmethd and class_mheadsD›)
\item all standard Exceptions are defined
\item all defined interfaces are wellformed
\item all defined classes are wellformed
\end{itemize}
›
definition
  wf_prog :: "prog  bool" where
 "wf_prog G = (let is = ifaces G; cs = classes G in
                 ObjectC  set cs  
                ( mset Object_mdecls. accmodi m  Package) 
                (xn. SXcptC xn  set cs) 
                (iset is. wf_idecl G i)  unique is 
                (cset cs. wf_cdecl G c)  unique cs)"

lemma wf_prog_idecl: "iface G I = Some i; wf_prog G  wf_idecl G (I,i)"
apply (unfold wf_prog_def Let_def)
apply simp
apply (fast dest: map_of_SomeD)
done

lemma wf_prog_cdecl: "class G C = Some c; wf_prog G  wf_cdecl G (C,c)"
apply (unfold wf_prog_def Let_def)
apply simp
apply (fast dest: map_of_SomeD)
done

lemma wf_prog_Object_mdecls:
"wf_prog G  ( mset Object_mdecls. accmodi m  Package)"
apply (unfold wf_prog_def Let_def)
apply simp
done

lemma wf_prog_acc_superD:
 "wf_prog G; class G C = Some c; C  Object  
   is_acc_class G (pid C) (super c)"
by (auto dest: wf_prog_cdecl wf_cdecl_supD)

lemma wf_ws_prog [elim!,simp]: "wf_prog G  ws_prog G"
apply (unfold wf_prog_def Let_def)
apply (rule ws_progI)
apply  (simp_all (no_asm))
apply  (auto simp add: is_acc_class_def is_acc_iface_def 
             dest!: wf_idecl_supD wf_cdecl_supD )+
done

lemma class_Object [simp]: 
"wf_prog G  
  class G Object = Some access=Public,cfields=[],methods=Object_mdecls,
                                  init=Skip,super=undefined,superIfs=[]"
apply (unfold wf_prog_def Let_def ObjectC_def)
apply (fast dest!: map_of_SomeI)
done

lemma methd_Object[simp]: "wf_prog G  methd G Object =  
  table_of (map (λ(s,m). (s, Object, m)) Object_mdecls)"
apply (subst methd_rec)
apply (auto simp add: Let_def)
done

lemma wf_prog_Object_methd:
"wf_prog G; methd G Object sig = Some m  accmodi m  Package"
by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 

lemma wf_prog_Object_is_public[intro]:
 "wf_prog G  is_public G Object"
by (auto simp add: is_public_def dest: class_Object)

lemma class_SXcpt [simp]: 
"wf_prog G  
  class G (SXcpt xn) = Some access=Public,cfields=[],methods=SXcpt_mdecls,
                                   init=Skip,
                                   super=if xn = Throwable then Object 
                                                           else SXcpt Throwable,
                                   superIfs=[]"
apply (unfold wf_prog_def Let_def SXcptC_def)
apply (fast dest!: map_of_SomeI)
done

lemma wf_ObjectC [simp]: 
        "wf_cdecl G ObjectC = (¬is_iface G Object  Ball (set Object_mdecls)
  (wf_mdecl G Object)  unique Object_mdecls)"
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
apply (auto intro: da.Skip)
done

lemma Object_is_class [simp,elim!]: "wf_prog G  is_class G Object"
apply (simp (no_asm_simp))
done
 
lemma Object_is_acc_class [simp,elim!]: "wf_prog G  is_acc_class G S Object"
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
                               accessible_in_RefT_simp)
done

lemma SXcpt_is_class [simp,elim!]: "wf_prog G  is_class G (SXcpt xn)"
apply (simp (no_asm_simp))
done

lemma SXcpt_is_acc_class [simp,elim!]: 
"wf_prog G  is_acc_class G S (SXcpt xn)"
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
                               accessible_in_RefT_simp)
done

lemma fields_Object [simp]: "wf_prog G  DeclConcepts.fields G Object = []"
by (force intro: fields_emptyI)

lemma accfield_Object [simp]: 
 "wf_prog G  accfield G S Object = Map.empty"
apply (unfold accfield_def)
apply (simp (no_asm_simp) add: Let_def)
done

lemma fields_Throwable [simp]: 
 "wf_prog G  DeclConcepts.fields G (SXcpt Throwable) = []"
by (force intro: fields_emptyI)

lemma fields_SXcpt [simp]: "wf_prog G  DeclConcepts.fields G (SXcpt xn) = []"
apply (case_tac "xn = Throwable")
apply  (simp (no_asm_simp))
by (force intro: fields_emptyI)

lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim]
lemma widen_trans2 [elim]: "GUT; GSU; wf_prog G  GST"
apply (erule (2) widen_trans)
done

lemma Xcpt_subcls_Throwable [simp]: 
"wf_prog G  GSXcpt xnC SXcpt Throwable"
apply (rule SXcpt_subcls_Throwable_lemma)
apply auto
done

lemma unique_fields: 
 "is_class G C; wf_prog G  unique (DeclConcepts.fields G C)"
apply (erule ws_unique_fields)
apply  (erule wf_ws_prog)
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
done

lemma fields_mono: 
"table_of (DeclConcepts.fields G C) fn = Some f; GDC C; 
  is_class G D; wf_prog G 
    table_of (DeclConcepts.fields G D) fn = Some f"
apply (rule map_of_SomeI)
apply  (erule (1) unique_fields)
apply (erule (1) map_of_SomeD [THEN fields_mono_lemma])
apply (erule wf_ws_prog)
done


lemma fields_is_type [elim]: 
"table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C  
      is_type G (type f)"
apply (frule wf_ws_prog)
apply (force dest: fields_declC [THEN conjunct1] 
                   wf_prog_cdecl [THEN wf_cdecl_fdecl]
             simp add: wf_fdecl_def2 is_acc_type_def)
done

lemma imethds_wf_mhead [rule_format (no_asm)]: 
"m  imethds G I sig; wf_prog G; is_iface G I   
  wf_mhead G (pid (decliface m)) sig (mthd m)  
  ¬ is_static m  accmodi m = Public"
apply (frule wf_ws_prog)
apply (drule (2) imethds_declI [THEN conjunct1])
apply clarify
apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption)
apply (drule wf_idecl_mhead)
apply (erule map_of_SomeD)
apply (cases m, simp)
done

lemma methd_wf_mdecl: 
 "methd G C sig = Some m; wf_prog G; class G C = Some y   
  GCC (declclass m)  is_class G (declclass m)  
  wf_mdecl G (declclass m) (sig,(mthd m))"
apply (frule wf_ws_prog)
apply (drule (1) methd_declC)
apply  fast
apply clarsimp
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
done

(*
This lemma doesn't hold!
lemma methd_rT_is_acc_type: 
"⟦wf_prog G;methd G C C sig = Some (D,m);
    class G C = Some y⟧
⟹ is_acc_type G (pid C) (resTy m)"
The result Type is only visible in the scope of defining class D 
"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C!
(The same is true for the type of pramaters of a method)
*)


lemma methd_rT_is_type: 
"wf_prog G;methd G C sig = Some m;
    class G C = Some y
 is_type G (resTy m)"
apply (drule (2) methd_wf_mdecl)
apply clarify
apply (drule wf_mdeclD1)
apply clarify
apply (drule rT_is_acc_type)
apply (cases m, simp add: is_acc_type_def)
done

lemma accmethd_rT_is_type:
"wf_prog G;accmethd G S C sig = Some m;
    class G C = Some y
 is_type G (resTy m)"
by (auto simp add: accmethd_def  
         intro: methd_rT_is_type)

lemma methd_Object_SomeD:
"wf_prog G;methd G Object sig = Some m 
  declclass m = Object"
by (auto dest: class_Object simp add: methd_rec )

lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P

lemma wf_imethdsD: 
 "im  imethds G I sig;wf_prog G; is_iface G I 
  ¬is_static im  accmodi im = Public"
proof -
  assume asm: "wf_prog G" "is_iface G I" "im  imethds G I sig"

  have "wf_prog G  
         ( i im. iface G I = Some i  im  imethds G I sig
                   ¬is_static im  accmodi im = Public)" (is "?P G I")
  proof (induct G I rule: iface_rec_induct', intro allI impI)
    fix G I i im
    assume hyp: " i J. iface G I = Some i  ws_prog G  J  set (isuperIfs i)
                  ?P G J"
    assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
           im: "im  imethds G I sig" 
    show "¬is_static im  accmodi im = Public" 
    proof -
      let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
      let ?new = "(set_option  table_of (map (λ(s, mh). (s, I, mh)) (imethods i)))"
      from if_I wf im have imethds:"im  (?inherited ⊕⊕ ?new) sig"
        by (simp add: imethds_rec)
      from wf if_I have 
        wf_supI: " J. J  set (isuperIfs i)  ( j. iface G J = Some j)"
        by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
      from wf if_I have
        " im  set (imethods i). ¬ is_static im  accmodi im = Public"
        by (auto dest!: wf_prog_idecl wf_idecl_mhead)
      then have new_ok: " im. table_of (imethods i) sig = Some im 
                           ¬ is_static im  accmodi im = Public"
        by (auto dest!: table_of_Some_in_set)
      show ?thesis
        proof (cases "?new sig = {}")
          case True
          from True wf wf_supI if_I imethds hyp 
          show ?thesis by (auto simp del:  split_paired_All)  
        next
          case False
          from False wf wf_supI if_I imethds new_ok hyp 
          show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
        qed
      qed
    qed
  with asm show ?thesis by (auto simp del: split_paired_All)
qed

lemma wf_prog_hidesD:
  assumes hides: "G new hides old" and wf: "wf_prog G"
  shows
   "accmodi old  accmodi new 
    is_static old"
proof -
  from hides 
  obtain c where 
    clsNew: "class G (declclass new) = Some c" and
    neqObj: "declclass new  Object"
    by (auto dest: hidesD declared_in_classD)
  with hides obtain newM oldM where
    newM: "table_of (methods c) (msig new) = Some newM" and 
     new: "new = (declclass new,(msig new),newM)" and
     old: "old = (declclass old,(msig old),oldM)" and
          "msig new = msig old"
    by (cases new,cases old) 
       (auto dest: hidesD 
         simp add: cdeclaredmethd_def declared_in_def)
  with hides 
  have hides':
        "G,(msig new)(declclass new,newM) hides (declclass old,oldM)"
    by auto
  from clsNew wf 
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
  note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
  with new old 
  show ?thesis
    by (cases new, cases old) auto
qed

text ‹Compare this lemma about static  
overriding termG new overridesS old with the definition of 
dynamic overriding termG new overrides old. 
Conforming result types and restrictions on the access modifiers of the old 
and the new method are not part of the predicate for static overriding. But
they are enshured in a wellfromed program.  Dynamic overriding has 
no restrictions on the access modifiers but enforces confrom result types 
as precondition. But with some efford we can guarantee the access modifier
restriction for dynamic overriding, too. See lemma 
wf_prog_dyn_override_prop›.
›
lemma wf_prog_stat_overridesD:
  assumes stat_override: "G new overridesS old" and wf: "wf_prog G"
  shows
   "GresTy newresTy old 
    accmodi old  accmodi new 
    ¬ is_static old"
proof -
  from stat_override 
  obtain c where 
    clsNew: "class G (declclass new) = Some c" and
    neqObj: "declclass new  Object"
    by (auto dest: stat_overrides_commonD declared_in_classD)
  with stat_override obtain newM oldM where
    newM: "table_of (methods c) (msig new) = Some newM" and 
     new: "new = (declclass new,(msig new),newM)" and
     old: "old = (declclass old,(msig old),oldM)" and
          "msig new = msig old"
    by (cases new,cases old) 
       (auto dest: stat_overrides_commonD 
         simp add: cdeclaredmethd_def declared_in_def)
  with stat_override 
  have stat_override':
        "G,(msig new)(declclass new,newM) overridesS (declclass old,oldM)"
    by auto
  from clsNew wf 
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
  note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
  with new old 
  show ?thesis
    by (cases new, cases old) auto
qed
    
lemma static_to_dynamic_overriding: 
  assumes stat_override: "Gnew overridesS old" and wf : "wf_prog G"
  shows "Gnew overrides old"
proof -
  from stat_override 
  show ?thesis (is "?Overrides new old")
  proof (induct)
    case (Direct new old superNew)
    then have stat_override:"Gnew overridesS old" 
      by (rule stat_overridesR.Direct)
    from stat_override wf
    have resTy_widen: "GresTy newresTy old" and
      not_static_old: "¬ is_static old" 
      by (auto dest: wf_prog_stat_overridesD)  
    have not_private_new: "accmodi new  Private"
    proof -
      from stat_override 
      have "accmodi old  Private"
        by (rule no_Private_stat_override)
      moreover
      from stat_override wf
      have "accmodi old  accmodi new"
        by (auto dest: wf_prog_stat_overridesD)
      ultimately
      show ?thesis
        by (auto dest: acc_modi_bottom)
    qed
    with Direct resTy_widen not_static_old 
    show "?Overrides new old" 
      by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
  next
    case (Indirect new inter old)
    then show "?Overrides new old" 
      by (blast intro: overridesR.Indirect) 
  qed
qed

lemma non_Package_instance_method_inheritance:
  assumes old_inheritable: "G⊢Method old inheritable_in (pid C)" and
              accmodi_old: "accmodi old  Package" and 
          instance_method: "¬ is_static old" and
                   subcls: "GC C declclass old" and
             old_declared: "G⊢Method old declared_in (declclass old)" and
                       wf: "wf_prog G"
  shows "G⊢Method old member_of C 
   ( new. G new overridesS old  G⊢Method new member_of C)"
proof -
  from wf have ws: "ws_prog G" by auto
  from old_declared have iscls_declC_old: "is_class G (declclass old)"
    by (auto simp add: declared_in_def cdeclaredmethd_def)
  from subcls have  iscls_C: "is_class G C"
    by (blast dest:  subcls_is_class)
  from iscls_C ws old_inheritable subcls 
  show ?thesis (is "?P C old")
  proof (induct rule: ws_class_induct')
    case Object
    assume "GObjectC declclass old"
    then show "?P Object old"
      by blast
  next
    case (Subcls C c)
    assume cls_C: "class G C = Some c" and 
       neq_C_Obj: "C  Object" and
             hyp: "G ⊢Method old inheritable_in pid (super c); 
                   Gsuper cC declclass old  ?P (super c) old" and
     inheritable: "G ⊢Method old inheritable_in pid C" and
         subclsC: "GCC declclass old"
    from cls_C neq_C_Obj  
    have super: "GC C1 super c" 
      by (rule subcls1I)
    from wf cls_C neq_C_Obj
    have accessible_super: "G(Class (super c)) accessible_in (pid C)" 
      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
    {
      fix old
      assume    member_super: "G⊢Method old member_of (super c)"
      assume     inheritable: "G ⊢Method old inheritable_in pid C"
      assume instance_method: "¬ is_static old"
      from member_super
      have old_declared: "G⊢Method old declared_in (declclass old)"
       by (cases old) (auto dest: member_of_declC)
      have "?P C old"
      proof (cases "Gmid (msig old) undeclared_in C")
        case True
        with inheritable super accessible_super member_super
        have "G⊢Method old member_of C"
          by (cases old) (auto intro: members.Inherited)
        then show ?thesis
          by auto
      next
        case False
        then obtain new_member where
             "Gnew_member declared_in C" and
             "mid (msig old) = memberid new_member"
          by (auto dest: not_undeclared_declared)
        then obtain new where
                  new: "G⊢Method new declared_in C" and
               eq_sig: "msig old = msig new" and
            declC_new: "declclass new = C" 
          by (cases new_member) auto
        then have member_new: "G⊢Method new member_of C"
          by (cases new) (auto intro: members.Immediate)
        from declC_new super member_super
        have subcls_new_old: "Gdeclclass new C declclass old"
          by (auto dest!: member_of_subclseq_declC
                    dest: r_into_trancl intro: trancl_rtrancl_trancl)
        show ?thesis
        proof (cases "is_static new")
          case False
          with eq_sig declC_new new old_declared inheritable
               super member_super subcls_new_old
          have "Gnew overridesS old"
            by (auto intro!: stat_overridesR.Direct)
          with member_new show ?thesis
            by blast
        next
          case True
          with eq_sig declC_new subcls_new_old new old_declared inheritable
          have "Gnew hides old"
            by (auto intro: hidesI)    
          with wf 
          have "is_static old"
            by (blast dest: wf_prog_hidesD)
          with instance_method
          show ?thesis
            by (contradiction)
        qed
      qed
    } note hyp_member_super = this
    from subclsC cls_C 
    have "G(super c)C declclass old"
      by (rule subcls_superD)
    then
    show "?P C old"
    proof (cases rule: subclseq_cases) 
      case Eq
      assume "super c = declclass old"
      with old_declared 
      have "G⊢Method old member_of (super c)" 
        by (cases old) (auto intro: members.Immediate)
      with inheritable instance_method 
      show ?thesis
        by (blast dest: hyp_member_super)
    next
      case Subcls
      assume "Gsuper cC declclass old"
      moreover
      from inheritable accmodi_old
      have "G ⊢Method old inheritable_in pid (super c)"
        by (cases "accmodi old") (auto simp add: inheritable_in_def)
      ultimately
      have "?P (super c) old"
        by (blast dest: hyp)
      then show ?thesis
      proof
        assume "G ⊢Method old member_of super c"
        with inheritable instance_method
        show ?thesis
          by (blast dest: hyp_member_super)
      next
        assume "new. G  new overridesS old  G ⊢Method new member_of super c"
        then obtain super_new where
          super_new_override:  "G  super_new overridesS old" and
            super_new_member:  "G ⊢Method super_new member_of super c"
          by blast
        from super_new_override wf
        have "accmodi old  accmodi super_new"
          by (auto dest: wf_prog_stat_overridesD)
        with inheritable accmodi_old
        have "G ⊢Method super_new inheritable_in pid C"
          by (auto simp add: inheritable_in_def 
                      split: acc_modi.splits
                       dest: acc_modi_le_Dests)
        moreover
        from super_new_override 
        have "¬ is_static super_new"
          by (auto dest: stat_overrides_commonD)
        moreover
        note super_new_member
        ultimately have "?P C super_new"
          by (auto dest: hyp_member_super)
        then show ?thesis
        proof 
          assume "G ⊢Method super_new member_of C"
          with super_new_override
          show ?thesis
            by blast
        next
          assume "new. G  new overridesS super_new  
                  G ⊢Method new member_of C"
          with super_new_override show ?thesis
            by (blast intro: stat_overridesR.Indirect) 
        qed
      qed
    qed
  qed
qed

lemma non_Package_instance_method_inheritance_cases:
  assumes old_inheritable: "G⊢Method old inheritable_in (pid C)" and
              accmodi_old: "accmodi old  Package" and 
          instance_method: "¬ is_static old" and
                   subcls: "GC C declclass old" and
             old_declared: "G⊢Method old declared_in (declclass old)" and
                       wf: "wf_prog G"
  obtains (Inheritance) "G⊢Method old member_of C"
    | (Overriding) new where "G new overridesS old" and "G⊢Method new member_of C"
proof -
  from old_inheritable accmodi_old instance_method subcls old_declared wf 
       Inheritance Overriding
  show thesis
    by (auto dest: non_Package_instance_method_inheritance)
qed

lemma dynamic_to_static_overriding:
  assumes dyn_override: "G new overrides old" and
           accmodi_old: "accmodi old  Package" and
                    wf: "wf_prog G"
  shows "G new overridesS old"  
proof - 
  from dyn_override accmodi_old
  show ?thesis (is "?Overrides new old")
  proof (induct rule: overridesR.induct)
    case (Direct new old)
    assume   new_declared: "G⊢Method new declared_in declclass new"
    assume eq_sig_new_old: "msig new = msig old"
    assume subcls_new_old: "Gdeclclass new C declclass old"
    assume "G ⊢Method old inheritable_in pid (declclass new)" and
           "accmodi old  Package" and
           "¬ is_static old" and
           "Gdeclclass newC declclass old" and
           "G⊢Method old declared_in declclass old" 
    from this wf
    show "?Overrides new old"
    proof (cases rule: non_Package_instance_method_inheritance_cases)
      case Inheritance
      assume "G ⊢Method old member_of declclass new"
      then have "Gmid (msig old) undeclared_in declclass new"
      proof cases
        case Immediate 
        with subcls_new_old wf show ?thesis     
          by (auto dest: subcls_irrefl)
      next
        case Inherited
        then show ?thesis
          by (cases old) auto
      qed
      with eq_sig_new_old new_declared
      show ?thesis
        by (cases old,cases new) (auto dest!: declared_not_undeclared)
    next
      case (Overriding new') 
      assume stat_override_new': "G  new' overridesS old"
      then have "msig new' = msig old"
        by (auto dest: stat_overrides_commonD)
      with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
        by simp
      assume "G ⊢Method new' member_of declclass new"
      then show ?thesis
      proof (cases)
        case Immediate
        then have declC_new: "declclass new' = declclass new" 
          by auto
        from Immediate 
        have "G⊢Method new' declared_in declclass new"
          by (cases new') auto
        with new_declared eq_sig_new_new' declC_new 
        have "new=new'"
          by (cases new, cases new') (auto dest: unique_declared_in) 
        with stat_override_new'
        show ?thesis
          by simp
      next
        case Inherited
        then have "Gmid (msig new') undeclared_in declclass new"
          by (cases new') (auto)
        with eq_sig_new_new' new_declared
        show ?thesis
          by (cases new,cases new') (auto dest!: declared_not_undeclared)
      qed
    qed
  next
    case (Indirect new inter old)
    assume accmodi_old: "accmodi old  Package"
    assume "accmodi old  Package  G  inter overridesS old"
    with accmodi_old 
    have stat_override_inter_old: "G  inter overridesS old"
      by blast
    moreover 
    assume hyp_inter: "accmodi inter  Package  G  new overridesS inter"
    moreover
    have "accmodi inter  Package"
    proof -
      from stat_override_inter_old wf 
      have "accmodi old  accmodi inter"
        by (auto dest: wf_prog_stat_overridesD)
      with stat_override_inter_old accmodi_old
      show ?thesis
        by (auto dest!: no_Private_stat_override
                 split: acc_modi.splits 
                 dest: acc_modi_le_Dests)
    qed
    ultimately show "?Overrides new old"
      by (blast intro: stat_overridesR.Indirect)
  qed
qed

lemma wf_prog_dyn_override_prop:
  assumes dyn_override: "G  new overrides old" and
                    wf: "wf_prog G"
  shows "accmodi old  accmodi new"
proof (cases "accmodi old = Package")
  case True
  note old_Package = this
  show ?thesis
  proof (cases "accmodi old  accmodi new")
    case True then show ?thesis .
  next
    case False
    with old_Package 
    have "accmodi new = Private"
      by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
    with dyn_override 
    show ?thesis
      by (auto dest: overrides_commonD)
  qed    
next
  case False
  with dyn_override wf
  have "G  new overridesS old"
    by (blast intro: dynamic_to_static_overriding)
  with wf 
  show ?thesis
   by (blast dest: wf_prog_stat_overridesD)
qed 

lemma overrides_Package_old: 
  assumes dyn_override: "G  new overrides old" and 
           accmodi_new: "accmodi new = Package" and
                    wf: "wf_prog G "
  shows "accmodi old = Package"
proof (cases "accmodi old")
  case Private
  with dyn_override show ?thesis
    by (simp add: no_Private_override)
next
  case Package
  then show ?thesis .
next
  case Protected
  with dyn_override wf
  have "G  new overridesS old"
    by (auto intro: dynamic_to_static_overriding)
  with wf 
  have "accmodi old  accmodi new"
    by (auto dest: wf_prog_stat_overridesD)
  with Protected accmodi_new
  show ?thesis
    by (simp add: less_acc_def le_acc_def)
next
  case Public
  with dyn_override wf
  have "G  new overridesS old"
    by (auto intro: dynamic_to_static_overriding)
  with wf 
  have "accmodi old  accmodi new"
    by (auto dest: wf_prog_stat_overridesD)
  with Public accmodi_new
  show ?thesis
    by (simp add: less_acc_def le_acc_def)
qed

lemma dyn_override_Package:
  assumes dyn_override: "G  new overrides old" and
           accmodi_old: "accmodi old = Package" and 
           accmodi_new: "accmodi new = Package" and
                    wf: "wf_prog G"
  shows "pid (declclass old) = pid (declclass new)"
proof - 
  from dyn_override accmodi_old accmodi_new
  show ?thesis (is "?EqPid old new")
  proof (induct rule: overridesR.induct)
    case (Direct new old)
    assume "accmodi old = Package"
           "G ⊢Method old inheritable_in pid (declclass new)"
    then show "pid (declclass old) =  pid (declclass new)"
      by (auto simp add: inheritable_in_def)
  next
    case (Indirect new inter old)
    assume accmodi_old: "accmodi old = Package" and
           accmodi_new: "accmodi new = Package" 
    assume "G  new overrides inter"
    with accmodi_new wf
    have "accmodi inter = Package"
      by  (auto intro: overrides_Package_old)
    with Indirect
    show "pid (declclass old) =  pid (declclass new)"
      by auto
  qed
qed

lemma dyn_override_Package_escape:
  assumes dyn_override: "G  new overrides old" and
           accmodi_old: "accmodi old = Package" and 
          outside_pack: "pid (declclass old)  pid (declclass new)" and
                    wf: "wf_prog G"
  shows " inter. G  new overrides inter  G  inter overrides old 
             pid (declclass old) = pid (declclass inter) 
             Protected  accmodi inter"
proof -
  from dyn_override accmodi_old outside_pack
  show ?thesis (is "?P new old")
  proof (induct rule: overridesR.induct)
    case (Direct new old)
    assume accmodi_old: "accmodi old = Package"
    assume outside_pack: "pid (declclass old)  pid (declclass new)"
    assume "G ⊢Method old inheritable_in pid (declclass new)"
    with accmodi_old 
    have "pid (declclass old) = pid (declclass new)"
      by (simp add: inheritable_in_def)
    with outside_pack 
    show "?P new old"
      by (contradiction)
  next
    case (Indirect new inter old)
    assume accmodi_old: "accmodi old = Package"
    assume outside_pack: "pid (declclass old)  pid (declclass new)"
    assume override_new_inter: "G  new overrides inter"
    assume override_inter_old: "G  inter overrides old"
    assume hyp_new_inter: "accmodi inter = Package; 
                           pid (declclass inter)  pid (declclass new)
                            ?P new inter"
    assume hyp_inter_old: "accmodi old = Package; 
                           pid (declclass old)  pid (declclass inter)
                            ?P inter old"
    show "?P new old"
    proof (cases "pid (declclass old) = pid (declclass inter)")
      case True
      note same_pack_old_inter = this
      show ?thesis
      proof (cases "pid (declclass inter) = pid (declclass new)")
        case True
        with same_pack_old_inter outside_pack
        show ?thesis
          by auto
      next
        case False
        note diff_pack_inter_new = this
        show ?thesis
        proof (cases "accmodi inter = Package")
          case True
          with diff_pack_inter_new hyp_new_inter  
          obtain newinter where
            over_new_newinter: "G  new overrides newinter" and
            over_newinter_inter: "G  newinter overrides inter" and 
            eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
            accmodi_newinter: "Protected  accmodi newinter"
            by auto
          from over_newinter_inter override_inter_old
          have "Gnewinter overrides old"
            by (rule overridesR.Indirect)
          moreover
          from eq_pid same_pack_old_inter 
          have "pid (declclass old) = pid (declclass newinter)"
            by simp
          moreover
          note over_new_newinter accmodi_newinter
          ultimately show ?thesis
            by blast
        next
          case False
          with override_new_inter
          have "Protected  accmodi inter"
            by (cases "accmodi inter") (auto dest: no_Private_override)
          with override_new_inter override_inter_old same_pack_old_inter
          show ?thesis
            by blast
        qed
      qed
    next
      case False
      with accmodi_old hyp_inter_old
      obtain newinter where
        over_inter_newinter: "G  inter overrides newinter" and
          over_newinter_old: "G  newinter overrides old" and 
                eq_pid: "pid (declclass old) = pid (declclass newinter)" and
        accmodi_newinter: "Protected  accmodi newinter"
        by auto
      from override_new_inter over_inter_newinter 
      have "G  new overrides newinter"
        by (rule overridesR.Indirect)
      with eq_pid over_newinter_old accmodi_newinter
      show ?thesis
        by blast
    qed
  qed
qed

lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P

lemma declclass_widen[rule_format]: 
 "wf_prog G 
  (c m. class G C = Some c  methd G C sig = Some m 
  GC C declclass m)" (is "?P G C")
proof (induct G C rule: class_rec_induct', intro allI impI)
  fix G C c m
  assume Hyp: "c. class G C = Some c  ws_prog G  C  Object
                ?P G (super c)"
  assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
         m:  "methd G C sig = Some m"
  show "GCC declclass m" 
  proof (cases "C=Object")
    case True 
    with wf m show ?thesis by (simp add: methd_Object_SomeD)
  next
    let ?filter="filter_tab (λsig m. GC inherits method sig m)"
    let ?table = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
    case False 
    with cls_C wf m
    have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
      by (simp add: methd_rec)
    show ?thesis
    proof (cases "?table sig")
      case None
      from this methd_C have "?filter (methd G (super c)) sig = Some m"
        by simp
      moreover
      from wf cls_C False obtain sup where "class G (super c) = Some sup"
        by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
      moreover note wf False cls_C  
      ultimately have "Gsuper c C declclass m"  
        by (auto intro: Hyp [rule_format])
      moreover from cls_C False have  "GC C1 super c" by (rule subcls1I)
      ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
    next
      case Some
      from this wf False cls_C methd_C show ?thesis by auto
    qed
  qed
qed

lemma declclass_methd_Object: 
 "wf_prog G; methd G Object sig = Some m  declclass m = Object"
by auto

lemma methd_declaredD: 
 "wf_prog G; is_class G C;methd G C sig = Some m 
   G(mdecl (sig,mthd m)) declared_in (declclass m)"
proof -
  assume    wf: "wf_prog G"
  then have ws: "ws_prog G" ..
  assume  clsC: "is_class G C"
  from clsC ws 
  show "methd G C sig = Some m 
         G(mdecl (sig,mthd m)) declared_in (declclass m)"
  proof (induct C rule: ws_class_induct')
    case Object
    assume "methd G Object sig = Some m" 
    with wf show ?thesis
      by - (rule method_declared_inI, auto) 
  next
    case Subcls
    fix C c
    assume clsC: "class G C = Some c"
    and       m: "methd G C sig = Some m"
    and     hyp: "methd G (super c) sig = Some m  ?thesis" 
    let ?newMethods = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
    show ?thesis
    proof (cases "?newMethods sig")
      case None
      from None ws clsC m hyp 
      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
    next
      case Some
      from Some ws clsC m 
      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
    qed
  qed
qed

lemma methd_rec_Some_cases:
  assumes methd_C: "methd G C sig = Some m" and
               ws: "ws_prog G" and
             clsC: "class G C = Some c" and
        neq_C_Obj: "CObject"
  obtains (NewMethod) "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig = Some m"
    | (InheritedMethod) "GC inherits (method sig m)" and "methd G (super c) sig = Some m"
proof -
  let ?inherited   = "filter_tab (λsig m. GC inherits method sig m) 
                              (methd G (super c))"
  let ?new = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
  from ws clsC neq_C_Obj methd_C 
  have methd_unfold: "(?inherited ++ ?new) sig = Some m"
    by (simp add: methd_rec)
  show thesis
  proof (cases "?new sig")
    case None
    with methd_unfold have "?inherited sig = Some m"
      by (auto)
    with InheritedMethod show ?thesis by blast
  next
    case Some
    with methd_unfold have "?new sig = Some m"
      by auto
    with NewMethod show ?thesis by blast
  qed
qed

  
lemma methd_member_of:
  assumes wf: "wf_prog G"
  shows
    "is_class G C; methd G C sig = Some m  G⊢Methd sig m member_of C" 
  (is "?Class C  ?Method C  ?MemberOf C") 
proof -
  from wf   have   ws: "ws_prog G" ..
  assume defC: "is_class G C"
  from defC ws 
  show "?Class C  ?Method C  ?MemberOf C"
  proof (induct rule: ws_class_induct')  
    case Object
    with wf have declC: "Object = declclass m"
      by (simp add: declclass_methd_Object)
    from Object wf have "G⊢Methd sig m declared_in Object"
      by (auto intro: methd_declaredD simp add: declC)
    with declC 
    show "?MemberOf Object"
      by (auto intro!: members.Immediate
                  simp del: methd_Object)
  next
    case (Subcls C c)
    assume  clsC: "class G C = Some c" and
       neq_C_Obj: "C  Object"  
    assume methd: "?Method C"
    from methd ws clsC neq_C_Obj
    show "?MemberOf C"
    proof (cases rule: methd_rec_Some_cases)
      case NewMethod
      with clsC show ?thesis
        by (auto dest: method_declared_inI intro!: members.Immediate)
    next
      case InheritedMethod
      then show "?thesis"
        by (blast dest: inherits_member)
    qed
  qed
qed

lemma current_methd: 
      "table_of (methods c) sig = Some new;
        ws_prog G; class G C = Some c; C  Object; 
        methd G (super c) sig = Some old 
     methd G C sig = Some (C,new)"
by (auto simp add: methd_rec
            intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)

lemma wf_prog_staticD:
  assumes     wf: "wf_prog G" and
            clsC: "class G C = Some c" and
       neq_C_Obj: "C  Object" and 
             old: "methd G (super c) sig = Some old" and 
     accmodi_old: "Protected  accmodi old" and
             new: "table_of (methods c) sig = Some new"
  shows "is_static new = is_static old"
proof -
  from clsC wf 
  have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
  from wf clsC neq_C_Obj
  have is_cls_super: "is_class G (super c)" 
    by (blast dest: wf_prog_acc_superD is_acc_classD)
  from wf is_cls_super old 
  have old_member_of: "G⊢Methd sig old member_of (super c)"  
    by (rule methd_member_of)
  from old wf is_cls_super 
  have old_declared: "G⊢Methd sig old declared_in (declclass old)"
    by (auto dest: methd_declared_in_declclass)
  from new clsC 
  have new_declared: "G⊢Methd sig (C,new) declared_in C"
    by (auto intro: method_declared_inI)
  note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
  from clsC neq_C_Obj
  have subcls1_C_super: "GC C1 super c"
    by (rule subcls1I)
  then have "GC C super c" ..
  also from old wf is_cls_super
  have "Gsuper c C (declclass old)" by (auto dest: methd_declC)
  finally have subcls_C_old:  "GC C (declclass old)" .
  from accmodi_old 
  have inheritable: "G⊢Methd sig old inheritable_in pid C"
    by (auto simp add: inheritable_in_def
                 dest: acc_modi_le_Dests)
  show ?thesis
  proof (cases "is_static new")
    case True
    with subcls_C_old new_declared old_declared inheritable
    have "G,sig(C,new) hides old"
      by (auto intro: hidesI)
    with True wf_cdecl neq_C_Obj new 
    show ?thesis
      by (auto dest: wf_cdecl_hides_SomeD)
  next
    case False
    with subcls_C_old new_declared old_declared inheritable subcls1_C_super
         old_member_of
    have "G,sig(C,new) overridesS old"
      by (auto intro: stat_overridesR.Direct)
    with False wf_cdecl neq_C_Obj new 
    show ?thesis
      by (auto dest: wf_cdecl_overrides_SomeD)
  qed
qed

lemma inheritable_instance_methd: 
  assumes subclseq_C_D: "GC C D" and
              is_cls_D: "is_class G D" and
                    wf: "wf_prog G" and 
                   old: "methd G D sig = Some old" and
           accmodi_old: "Protected  accmodi old" and  
        not_static_old: "¬ is_static old"
  shows
  "new. methd G C sig = Some new 
         (new = old  G,signew overridesS old)"
 (is "(new. (?Constraint C new old))")
proof -
  from subclseq_C_D is_cls_D 
  have is_cls_C: "is_class G C" by (rule subcls_is_class2) 
  from wf 
  have ws: "ws_prog G" ..
  from is_cls_C ws subclseq_C_D 
  show "new. ?Constraint C new old"
  proof (induct rule: ws_class_induct')
    case (Object co)
    then have eq_D_Obj: "D=Object" by auto
    with old 
    have "?Constraint Object old old"
      by auto
    with eq_D_Obj 
    show " new. ?Constraint Object new old" by auto
  next
    case (Subcls C c)
    assume hyp: "Gsuper cC D  new. ?Constraint (super c) new old"
    assume clsC: "class G C = Some c"
    assume neq_C_Obj: "CObject"
    from clsC wf 
    have wf_cdecl: "wf_cdecl G (C,c)" 
      by (rule wf_prog_cdecl)
    from ws clsC neq_C_Obj
    have is_cls_super: "is_class G (super c)"
      by (auto dest: ws_prog_cdeclD)
    from clsC wf neq_C_Obj 
    have superAccessible: "G(Class (super c)) accessible_in (pid C)" and
         subcls1_C_super: "GC C1 super c"
      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
              intro: subcls1I)
    show "new. ?Constraint C new old"
    proof (cases "Gsuper cC D")
      case False
      from False Subcls 
      have eq_C_D: "C=D"
        by (auto dest: subclseq_superD)
      with old 
      have "?Constraint C old old"
        by auto
      with eq_C_D 
      show " new. ?Constraint C new old" by auto
    next
      case True
      with hyp obtain super_method
        where super: "?Constraint (super c) super_method old" by blast
      from super not_static_old
      have not_static_super: "¬ is_static super_method"
        by (auto dest!: stat_overrides_commonD)
      from super old wf accmodi_old
      have accmodi_super_method: "Protected  accmodi super_method"
        by (auto dest!: wf_prog_stat_overridesD)
      from super accmodi_old wf
      have inheritable: "G⊢Methd sig super_method inheritable_in (pid C)"
        by (auto dest!: wf_prog_stat_overridesD
                        acc_modi_le_Dests
              simp add: inheritable_in_def)                
      from super wf is_cls_super
      have member: "G⊢Methd sig super_method member_of (super c)"
        by (auto intro: methd_member_of) 
      from member
      have decl_super_method:
        "G⊢Methd sig super_method declared_in (declclass super_method)"
        by (auto dest: member_of_declC)
      from super subcls1_C_super ws is_cls_super 
      have subcls_C_super: "GC C (declclass super_method)"
        by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 
      show " new. ?Constraint C new old"
      proof (cases "methd G C sig")
        case None
        have "methd G (super c) sig = None"
        proof -
          from clsC ws None 
          have no_new: "table_of (methods c) sig = None" 
            by (auto simp add: methd_rec)
          with clsC 
          have undeclared: "Gmid sig undeclared_in C"
            by (auto simp add: undeclared_in_def cdeclaredmethd_def)
          with inheritable member superAccessible subcls1_C_super
          have inherits: "GC inherits (method sig super_method)"
            by (auto simp add: inherits_def)
          with clsC ws no_new super neq_C_Obj
          have "methd G C sig = Some super_method"
            by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
          with None show ?thesis
            by simp
        qed
        with super show ?thesis by auto
      next
        case (Some new)
        from this ws clsC neq_C_Obj
        show ?thesis
        proof (cases rule: methd_rec_Some_cases)
          case InheritedMethod
          with super Some show ?thesis 
            by auto
        next
          case NewMethod
          assume new: "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig 
                       = Some new"
          from new 
          have declcls_new: "declclass new = C" 
            by auto
          from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
          have not_static_new: "¬ is_static new" 
            by (auto dest: wf_prog_staticD) 
          from clsC new
          have decl_new: "G⊢Methd sig new declared_in C"
            by (auto simp add: declared_in_def cdeclaredmethd_def)
          from not_static_new decl_new decl_super_method
               member subcls1_C_super inheritable declcls_new subcls_C_super 
          have "G,sig new overridesS super_method"
            by (auto intro: stat_overridesR.Direct) 
          with super Some
          show ?thesis
            by (auto intro: stat_overridesR.Indirect)
        qed
      qed
    qed
  qed
qed

lemma inheritable_instance_methd_cases:
  assumes subclseq_C_D: "GC C D" and
              is_cls_D: "is_class G D" and
                    wf: "wf_prog G" and 
                   old: "methd G D sig = Some old" and
           accmodi_old: "Protected  accmodi old" and  
        not_static_old: "¬ is_static old"
  obtains (Inheritance) "methd G C sig = Some old"
    | (Overriding) new where "methd G C sig = Some new" and "G,signew overridesS old"
proof -
  from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  show ?thesis
    by (auto dest: inheritable_instance_methd intro: Inheritance Overriding)
qed

lemma inheritable_instance_methd_props: 
  assumes subclseq_C_D: "GC C D" and
              is_cls_D: "is_class G D" and
                    wf: "wf_prog G" and 
                   old: "methd G D sig = Some old" and
           accmodi_old: "Protected  accmodi old" and  
        not_static_old: "¬ is_static old"
  shows
  "new. methd G C sig = Some new 
          ¬ is_static new  GresTy newresTy old  accmodi old accmodi new"
 (is "(new. (?Constraint C new old))")
proof -
  from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
  show ?thesis
  proof (cases rule: inheritable_instance_methd_cases)
    case Inheritance
    with not_static_old accmodi_old show ?thesis by auto
  next
    case (Overriding new)
    then have "¬ is_static new" by (auto dest: stat_overrides_commonD)
    with Overriding not_static_old accmodi_old wf 
    show ?thesis 
      by (auto dest!: wf_prog_stat_overridesD)
  qed
qed
              
(* local lemma *)
lemma bexI': "x  A  P x  xA. P x" by blast
lemma ballE': "xA. P x  (x  A  Q)  (P x  Q)  Q" by blast

lemma subint_widen_imethds: 
  assumes irel: "GI≼I J"
  and wf: "wf_prog G"
  and is_iface: "is_iface G J"
  and jm: "jm  imethds G J sig"
  shows "im  imethds G I sig. is_static im = is_static jm  
                          accmodi im = accmodi jm 
                          GresTy imresTy jm"
  using irel jm
proof (induct rule: converse_rtrancl_induct)
    case base
    then show ?case by  (blast elim: bexI')
  next
    case (step I SI)
    from GI ≺I1 SI
    obtain i where
      ifI: "iface G I = Some i" and
       SI: "SI  set (isuperIfs i)"
      by (blast dest: subint1D)

    let ?newMethods 
          = "(set_option  table_of (map (λ(sig, mh). (sig, I, mh)) (imethods i)))"
    show ?case
    proof (cases "?newMethods sig = {}")
      case True
      with ifI SI step wf
      show "?thesis" 
        by (auto simp add: imethds_rec) 
    next
      case False
      from ifI wf False
      have imethds: "imethds G I sig = ?newMethods sig"
        by (simp add: imethds_rec)
      from False
      obtain im where
        imdef: "im  ?newMethods sig" 
        by (blast)
      with imethds 
      have im: "im  imethds G I sig"
        by (blast)
      with im wf ifI 
      obtain
         imStatic: "¬ is_static im" and
         imPublic: "accmodi im = Public"
        by (auto dest!: imethds_wf_mhead)       
      from ifI wf 
      have wf_I: "wf_idecl G (I,i)" 
        by (rule wf_prog_idecl)
      with SI wf  
      obtain si where
         ifSI: "iface G SI = Some si" and
        wf_SI: "wf_idecl G (SI,si)" 
        by (auto dest!: wf_idecl_supD is_acc_ifaceD
                  dest: wf_prog_idecl)
      from step
      obtain sim::"qtname × mhead"  where
                      sim: "sim  imethds G SI sig" and
         eq_static_sim_jm: "is_static sim = is_static jm" and 
         eq_access_sim_jm: "accmodi sim = accmodi jm" and 
        resTy_widen_sim_jm: "GresTy simresTy jm"
        by blast
      with wf_I SI imdef sim 
      have "GresTy imresTy sim"   
        by (auto dest!: wf_idecl_hidings hidings_entailsD)
      with wf resTy_widen_sim_jm 
      have resTy_widen_im_jm: "GresTy imresTy jm"
        by (blast intro: widen_trans)
      from sim wf ifSI  
      obtain
        simStatic: "¬ is_static sim" and
        simPublic: "accmodi sim = Public"
        by (auto dest!: imethds_wf_mhead)
      from im 
           imStatic simStatic eq_static_sim_jm
           imPublic simPublic eq_access_sim_jm
           resTy_widen_im_jm
      show ?thesis 
        by auto 
    qed
qed
     
(* Tactical version *)
(* 
lemma subint_widen_imethds: "⟦G⊢I≼I J; wf_prog G; is_iface G J⟧ ⟹  
  ∀ jm ∈ imethds G J sig.  
  ∃ im ∈ imethds G I sig. static (mthd im)=static (mthd jm) ∧ 
                          access (mthd im)= access (mthd jm) ∧
                          G⊢resTy (mthd im)≼resTy (mthd jm)"
apply (erule converse_rtrancl_induct)
apply  (clarsimp elim!: bexI')
apply (frule subint1D)
apply clarify
apply (erule ballE')
apply  fast
apply (erule_tac V = "?x ∈ imethds G J sig" in thin_rl)
apply clarsimp
apply (subst imethds_rec, assumption, erule wf_ws_prog)
apply (unfold overrides_t_def)
apply (drule (1) wf_prog_idecl)
apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
                                       [THEN is_acc_ifaceD [THEN conjunct1]]]])
apply (case_tac "(set_option ∘ table_of (map (λ(s, mh). (s, y, mh)) (imethods i)))
                  sig ={}")
apply   force

apply   (simp only:)
apply   (simp)
apply   clarify
apply   (frule wf_idecl_hidings [THEN hidings_entailsD])
apply     blast
apply     blast
apply   (rule bexI')
apply     simp
apply     (drule table_of_map_SomeI [of _ "sig"])
apply     simp

apply     (frule wf_idecl_mhead [of _ _ _ "sig"])
apply       (rule table_of_Some_in_set)
apply       assumption
apply     auto
done
*)
    

(* local lemma *)
lemma implmt1_methd: 
 "sig. GC↝1I; wf_prog G; im  imethds G I sig   
  cm methd G C sig: ¬ is_static cm  ¬ is_static im  
                       GresTy cmresTy im 
                       accmodi im = Public  accmodi cm = Public"
apply (drule implmt1D)
apply clarify
apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
apply (frule (1) imethds_wf_mhead)
apply  (simp add: is_acc_iface_def)
apply (force)
done


(* local lemma *)
lemma implmt_methd [rule_format (no_asm)]: 
"wf_prog G; GCI  is_iface G I   
 ( im    imethds G I   sig.  
   cmmethd G C sig: ¬is_static cm  ¬ is_static im  
                      GresTy cmresTy im 
                      accmodi im = Public  accmodi cm = Public)"
apply (frule implmt_is_class)
apply (erule implmt.induct)
apply   safe
apply   (drule (2) implmt1_methd)
apply   fast
apply  (drule (1) subint_widen_imethds)
apply   simp
apply   assumption
apply  clarify
apply  (drule (2) implmt1_methd)
apply  (force)
apply (frule subcls1D)
apply (drule (1) bspec)
apply clarify
apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 
                                 OF _ implmt_is_class])
apply auto 
done

lemma mheadsD [rule_format (no_asm)]: 
"emh  mheads G S t sig  wf_prog G 
 (C D m. t = ClassT C  declrefT emh = ClassT D  
          accmethd G S C sig = Some m 
          (declclass m = D)  mhead (mthd m) = (mhd emh)) 
 (I. t = IfaceT I  ((im. im   accimethds G (pid S) I sig  
          mthd im = mhd emh)  
  (m. GIface I accessible_in (pid S)  accmethd G S Object sig = Some m  
       accmodi m  Private  
       declrefT emh = ClassT Object  mhead (mthd m) = mhd emh))) 
 (T m. t = ArrayT T  GArray T accessible_in (pid S) 
        accmethd G S Object sig = Some m  accmodi m  Private  
        declrefT emh = ClassT Object  mhead (mthd m) = mhd emh)"
apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1])
apply auto
apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
apply (auto  dest!: accmethd_SomeD)
done

lemma mheads_cases:
  assumes "emh  mheads G S t sig" and "wf_prog G"
  obtains (Class_methd) C D m where
      "t = ClassT C" "declrefT emh = ClassT D" "accmethd G S C sig = Some m"
      "declclass m = D" "mhead (mthd m) = mhd emh"
    | (Iface_methd) I im where "t = IfaceT I"
        "im   accimethds G (pid S) I sig" "mthd im = mhd emh"
    | (Iface_Object_methd) I m where
        "t = IfaceT I" "GIface I accessible_in (pid S)"
        "accmethd G S Object sig = Some m" "accmodi m  Private"
        "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
    | (Array_Object_methd) T m where
        "t = ArrayT T" "GArray T accessible_in (pid S)"
        "accmethd G S Object sig = Some m" "accmodi m  Private"
        "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
using assms by (blast dest!: mheadsD)

lemma declclassD[rule_format]:
 "wf_prog G;class G C = Some c; methd G C sig = Some m; 
   class G (declclass m) = Some d
   table_of (methods d) sig  = Some (mthd m)"
proof -
  assume    wf: "wf_prog G"
  then have ws: "ws_prog G" ..
  assume  clsC: "class G C = Some c"
  from clsC ws 
  show " m d. methd G C sig = Some m; class G (declclass m) = Some d
         table_of (methods d) sig  = Some (mthd m)" 
  proof (induct rule: ws_class_induct)
    case Object
    with wf show "?thesis m d" by auto
  next
    case (Subcls C c)
    let ?newMethods = "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig"
    show "?thesis m d" 
    proof (cases "?newMethods")
      case None
      from None ws Subcls
      show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
    next
      case Some
      from Some ws Subcls
      show "?thesis" 
        by (auto simp add: methd_rec
                     dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
    qed
  qed
qed

lemma dynmethd_Object:
  assumes statM: "methd G Object sig = Some statM" and
        "private": "accmodi statM = Private" and 
       is_cls_C: "is_class G C" and
             wf: "wf_prog G"
  shows "dynmethd G Object C sig = Some statM"
proof -
  from is_cls_C wf 
  have subclseq: "GC C Object" 
    by (auto intro: subcls_ObjectI)
  from wf have ws: "ws_prog G" 
    by simp
  from wf 
  have is_cls_Obj: "is_class G Object" 
    by simp
  from statM subclseq is_cls_Obj ws "private"
  show ?thesis
  proof (cases rule: dynmethd_cases)
    case Static then show ?thesis .
  next
    case Overrides 
    with "private" show ?thesis 
      by (auto dest: no_Private_override)
  qed
qed

lemma wf_imethds_hiding_objmethdsD: 
  assumes     old: "methd G Object sig = Some old" and
          is_if_I: "is_iface G I" and
               wf: "wf_prog G" and    
      not_private: "accmodi old  Private" and
              new: "new  imethds G I sig" 
  shows "GresTy newresTy old  is_static new = is_static old" (is "?P new")
proof -
  from wf have ws: "ws_prog G" by simp
  {
    fix I i new
    assume ifI: "iface G I = Some i"
    assume new: "table_of (imethods i) sig = Some new" 
    from ifI new not_private wf old  
    have "?P (I,new)"
      by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
            simp del: methd_Object)
  } note hyp_newmethod = this  
  from is_if_I ws new 
  show ?thesis
  proof (induct rule: ws_interface_induct)
    case (Step I i)
    assume ifI: "iface G I = Some i" 
    assume new: "new  imethds G I sig" 
    from Step
    have hyp: " J  set (isuperIfs i). (new  imethds G J sig  ?P new)"
      by auto 
    from new ifI ws
    show "?P new"
    proof (cases rule: imethds_cases)
      case NewMethod
      with ifI hyp_newmethod
      show ?thesis
        by auto
    next
      case (InheritedMethod J)
      assume "J  set (isuperIfs i)" 
             "new  imethds G J sig"
      with hyp 
      show "?thesis"
        by auto
    qed
  qed
qed

text ‹
Which dynamic classes are valid to look up a member of a distinct static type?
We have to distinct class members (named static members in Java) 
from instance members. Class members are global to all Objects of a class,
instance members are local to a single Object instance. If a member is
equipped with the static modifier it is a class member, else it is an 
instance member.
The following table gives an overview of the current framework. We assume
to have a reference with static type statT and a dynamic class dynC. Between
both of these types the widening relation holds 
termGClass dynC statT. Unfortunately this ordinary widening relation 
isn't enough to describe the valid lookup classes, since we must cope the
special cases of arrays and interfaces,too. If we statically expect an array or
inteface we may lookup a field or a method in Object which isn't covered in 
the widening relation.

statT      field         instance method       static (class) method
------------------------------------------------------------------------
 NullT      /                  /                   /
 Iface      /                dynC                Object
 Class    dynC               dynC                 dynC
 Array      /                Object              Object

In most cases we con lookup the member in the dynamic class. But as an
interface can't declare new static methods, nor an array can define new
methods at all, we have to lookup methods in the base class Object.

The limitation to classes in the field column is artificial  and comes out
of the typing rule for the field access (see rule FVar› in the 
welltyping relation termwt in theory WellType). 
I stems out of the fact, that Object
indeed has no non private fields. So interfaces and arrays can actually
have no fields at all and a field access would be senseless. (In Java
interfaces are allowed to declare new fields but in current Bali not!).
So there is no principal reason why we should not allow Objects to declare
non private fields. Then we would get the following column:
       
 statT    field
----------------- 
 NullT      /  
 Iface    Object 
 Class    dynC 
 Array    Object
›
primrec valid_lookup_cls:: "prog  ref_ty  qtname  bool  bool"
                        ("_,_  _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
where
  "G,NullT     dynC valid_lookup_cls_for static_membr = False"
| "G,IfaceT I  dynC valid_lookup_cls_for static_membr 
                = (if static_membr 
                      then dynC=Object 
                      else GClass dynC Iface I)"
| "G,ClassT C  dynC valid_lookup_cls_for static_membr = GClass dynC Class C"
| "G,ArrayT T  dynC valid_lookup_cls_for static_membr = (dynC=Object)"

lemma valid_lookup_cls_is_class:
  assumes dynC: "G,statT  dynC valid_lookup_cls_for static_membr" and
      ty_statT: "isrtype G statT" and
            wf: "wf_prog G"
  shows "is_class G dynC"
proof (cases statT)
  case NullT
  with dynC ty_statT show ?thesis
    by (auto dest: widen_NT2)
next
  case (IfaceT I)
  with dynC wf show ?thesis
    by (auto dest: implmt_is_class)
next
  case (ClassT C)
  with dynC ty_statT show ?thesis
    by (auto dest: subcls_is_class2)
next
  case (ArrayT T)
  with dynC wf show ?thesis
    by (auto)
qed

declare split_paired_All [simp del] split_paired_Ex [simp del]
setup map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")
setup map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")

lemma dynamic_mheadsD:   
"emh  mheads G S statT sig;    
  G,statT  dynC valid_lookup_cls_for (is_static emh);
  isrtype G statT; wf_prog G
   m  dynlookup G statT dynC sig: 
          is_static m=is_static emh  GresTy mresTy emh"
proof - 
  assume      emh: "emh  mheads G S statT sig"
  and          wf: "wf_prog G"
  and   dynC_Prop: "G,statT  dynC valid_lookup_cls_for (is_static emh)"
  and      istype: "isrtype G statT"
  from dynC_Prop istype wf 
  obtain y where
    dynC: "class G dynC = Some y" 
    by (auto dest: valid_lookup_cls_is_class)
  from emh wf show ?thesis
  proof (cases rule: mheads_cases)
    case Class_methd
    fix statC statDeclC sm
    assume     statC: "statT = ClassT statC"
    assume            "accmethd G S statC sig = Some sm"
    then have     sm: "methd G statC sig = Some sm" 
      by (blast dest: accmethd_SomeD)  
    assume eq_mheads: "mhead (mthd sm) = mhd emh"
    from statC 
    have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
      by (simp add: dynlookup_def)
    from wf statC istype dynC_Prop sm 
    obtain dm where
      "dynmethd G statC dynC sig = Some dm"
      "is_static dm = is_static sm" 
      "GresTy dmresTy sm"  
      by (force dest!: ws_dynmethd accmethd_SomeD)
    with dynlookup eq_mheads 
    show ?thesis 
      by (cases emh type: prod) (auto)
  next
    case Iface_methd
    fix I im
    assume    statI: "statT = IfaceT I" and
          eq_mheads: "mthd im = mhd emh" and
                     "im  accimethds G (pid S) I sig" 
    then have im: "im  imethds G I sig" 
      by (blast dest: accimethdsD)
    with istype statI eq_mheads wf 
    have not_static_emh: "¬ is_static emh"
      by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
    from statI im
    have dynlookup: "dynlookup G statT dynC sig = methd G dynC</