(* 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) ∧ ( ∀T∈set (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) ∧ (∀pn∈set (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); ∀T∈set (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)); (∀pn∈set (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)); ∀pn∈set (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)) ∧ (∀pn∈set (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 m⦈⊢Body C (stmt (mbody m))∷-T ∧ G⊢T≼(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) ∧ (∀ J∈set (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. G⊢resTy new≼resTy 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. G⊢resTy new≼resTy 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. G⊢resTy new≼resTy 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. G⊢resTy new≼resTy 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 ∧ (∀I∈set (superIfs c). is_acc_iface G (pid C) I ∧ (∀s. ∀ im ∈ imethds G I s. (∃ cm ∈ methd G C s: G⊢resTy cm≼resTy 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) ∧ 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,sig⊢new overrides⇩_{S}old ⟶ (G⊢resTy new≼resTy old ∧ accmodi old ≤ accmodi new ∧ ¬is_static old)) ∧ (G,sig⊢new 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; (∀I∈set (superIfs c). is_acc_iface G (pid C) I ∧ (∀s. ∀ im ∈ imethds G I s. (∃ cm ∈ methd G C s: G⊢resTy cm≼resTy 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); 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,sig⊢new overrides⇩_{S}old ⟶ (G⊢resTy new≼resTy old ∧ accmodi old ≤ accmodi new ∧ ¬is_static old)) ∧ (G,sig⊢new 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); f∈set (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); m∈set (methods c)⟧ ⟹ wf_mdecl G C m" apply (unfold wf_cdecl_def) apply auto done lemma wf_cdecl_impD: "⟦wf_cdecl G (C,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 cm≼resTy 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,sig⊢new overrides⇩_{S}old ⟶ (G⊢resTy new≼resTy old ∧ accmodi old ≤ accmodi new ∧ ¬is_static old)) ∧ (G,sig⊢new 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) overrides⇩_{S}old ⟧ ⟹ G⊢resTy newM≼resTy 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.empty⦈⊢init 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 ∧ (∀ m∈set Object_mdecls. accmodi m ≠ Package) ∧ (∀xn. SXcptC xn ∈ set cs) ∧ (∀i∈set is. wf_idecl G i) ∧ unique is ∧ (∀c∈set 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 ⟹ (∀ m∈set 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]: "⟦G⊢U≼T; G⊢S≼U; wf_prog G⟧ ⟹ G⊢S≼T" apply (erule (2) widen_trans) done lemma Xcpt_subcls_Throwable [simp]: "wf_prog G ⟹ G⊢SXcpt xn≼⇩_{C}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; G⊢D≼⇩_{C}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⟧ ⟹ G⊢C≼⇩_{C}(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 \<^term>‹G ⊢new overrides⇩_{S}old› with the definition of dynamic overriding \<^term>‹G ⊢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 overrides⇩_{S}old" and wf: "wf_prog G" shows "G⊢resTy new≼resTy 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) overrides⇩_{S}(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: "G⊢new overrides⇩_{S}old" and wf : "wf_prog G" shows "G⊢new overrides old" proof - from stat_override show ?thesis (is "?Overrides new old") proof (induct) case (Direct new old superNew) then have stat_override:"G⊢new overrides⇩_{S}old" by (rule stat_overridesR.Direct) from stat_override wf have resTy_widen: "G⊢resTy new≼resTy 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: "G⊢C ≺⇩_{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 overrides⇩_{S}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 "G⊢Object≺⇩_{C}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); G⊢super c≺⇩_{C}declclass old⟧ ⟹ ?P (super c) old" and inheritable: "G ⊢Method old inheritable_in pid C" and subclsC: "G⊢C≺⇩_{C}declclass old" from cls_C neq_C_Obj have super: "G⊢C ≺⇩_{C}1 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 "G⊢mid (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 "G⊢new_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: "G⊢declclass 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 "G⊢new overrides⇩_{S}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 "G⊢new 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 "G⊢super c≺⇩_{C}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 overrides⇩_{S}old ∧ G ⊢Method new member_of super c" then obtain super_new where super_new_override: "G ⊢ super_new overrides⇩_{S}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 overrides⇩_{S}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: "G⊢C ≺⇩_{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 overrides⇩_{S}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 overrides⇩_{S}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: "G⊢declclass new ≺⇩_{C}declclass old" assume "G ⊢Method old inheritable_in pid (declclass new)" and "accmodi old ≠ Package" and "¬ is_static old" and "G⊢declclass new≺⇩_{C}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 "G⊢mid (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' overrides⇩_{S}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 "G⊢mid (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 overrides⇩_{S}old" with accmodi_old have stat_override_inter_old: "G ⊢ inter overrides⇩_{S}old" by blast moreover assume hyp_inter: "accmodi inter ≠ Package ⟹ G ⊢ new overrides⇩_{S}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 overrides⇩_{S}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 overrides⇩_{S}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 overrides⇩_{S}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 "G⊢newinter 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 ⟶ G⊢C ≼⇩_{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 "G⊢C≼⇩_{C}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. G⊢C 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 "G⊢super c ≼⇩_{C}declclass m" by (auto intro: Hyp [rule_format]) moreover from cls_C False have "G⊢C ≺⇩_{C}1 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: "C≠Object" obtains (NewMethod) "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig = Some m" | (InheritedMethod) "G⊢C inherits (method sig m)" and "methd G (super c) sig = Some m" proof - let ?inherited = "filter_tab (λsig m. G⊢C 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: "G⊢C ≺⇩_{C}1 super c" by (rule subcls1I) then have "G⊢C ≺⇩_{C}super c" .. also from old wf is_cls_super have "G⊢super c ≼⇩_{C}(declclass old)" by (auto dest: methd_declC) finally have subcls_C_old: "G⊢C ≺⇩_{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) overrides⇩_{S}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: "G⊢C ≼⇩_{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,sig⊢new overrides⇩_{S}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: "G⊢super c≼⇩_{C}D ⟹ ∃new. ?Constraint (super c) new old" assume clsC: "class G C = Some c" assume neq_C_Obj: "C≠Object" 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: "G⊢C ≺⇩_{C}1 super c" by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD intro: subcls1I) show "∃new. ?Constraint C new old" proof (cases "G⊢super c≼⇩_{C}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: "G⊢C ≺⇩_{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: "G⊢mid sig undeclared_in C" by (auto simp add: undeclared_in_def cdeclaredmethd_def) with inheritable member superAccessible subcls1_C_super have inherits: "G⊢C 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 overrides⇩_{S}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: "G⊢C ≼⇩_{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,sig⊢new overrides⇩_{S}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: "G⊢C ≼⇩_{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 ∧ G⊢resTy new≼resTy 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 ⟹ ∃x∈A. P x" by blast lemma ballE': "∀x∈A. P x ⟹ (x ∉ A ⟹ Q) ⟹ (P x ⟹ Q) ⟹ Q" by blast lemma subint_widen_imethds: assumes irel: "G⊢I≼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 ∧ G⊢resTy im≼resTy 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 ‹G⊢I ≺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: "G⊢resTy sim≼resTy jm" by blast with wf_I SI imdef sim have "G⊢resTy im≼resTy sim" by (auto dest!: wf_idecl_hidings hidings_entailsD) with wf resTy_widen_sim_jm have resTy_widen_im_jm: "G⊢resTy im≼resTy 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. ⟦G⊢C↝1I; wf_prog G; im ∈ imethds G I sig⟧ ⟹ ∃cm ∈methd G C sig: ¬ is_static cm ∧ ¬ is_static im ∧ G⊢resTy cm≼resTy 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; G⊢C↝I⟧ ⟹ is_iface G I ⟶ (∀ im ∈imethds G I sig. ∃ cm∈methd G C sig: ¬is_static cm ∧ ¬ is_static im ∧ G⊢resTy cm≼resTy 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. G⊢Iface 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 ∧ G⊢Array 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" "G⊢Iface 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" "G⊢Array 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: "G⊢C ≼⇩_{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 "G⊢resTy new≼resTy 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 \<^term>‹G⊢Class 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 \<^term>‹wt› 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 G⊢Class dynC≼ Iface I)" | "G,ClassT C ⊢ dynC valid_lookup_cls_for static_membr = G⊢Class 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 ∧ G⊢resTy m≼resTy 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" "G⊢resTy dm≼resTy 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</