(* Title: HOL/Bali/TypeRel.thy ID: $Id: TypeRel.thy,v 1.8 2005/06/17 14:13:06 haftmann Exp $ Author: David von Oheimb *) header {* The relations between Java types *} theory TypeRel imports Decl begin text {* simplifications: \begin{itemize} \item subinterface, subclass and widening relation includes identity \end{itemize} improvements over Java Specification 1.0: \begin{itemize} \item narrowing reference conversion also in cases where the return types of a pair of methods common to both types are in widening (rather identity) relation \item one could add similar constraints also for other cases \end{itemize} design issues: \begin{itemize} \item the type relations do not require @{text is_type} for their arguments \item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class} for their first arguments, which is required for their finiteness \end{itemize} *} consts (*subint1, in Decl.thy*) (* direct subinterface *) (*subint , by translation*) (* subinterface (+ identity) *) (*subcls1, in Decl.thy*) (* direct subclass *) (*subcls , by translation*) (* subclass *) (*subclseq, by translation*) (* subclass + identity *) implmt1 :: "prog => (qtname × qtname) set" --{* direct implementation *} implmt :: "prog => (qtname × qtname) set" --{* implementation *} widen :: "prog => (ty × ty ) set" --{* widening *} narrow :: "prog => (ty × ty ) set" --{* narrowing *} cast :: "prog => (ty × ty ) set" --{* casting *} syntax "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70) "@subint" :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70) (* Defined in Decl.thy: "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70) "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70) "@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70) *) "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70) "@implmt" :: "prog => [qtname, qtname] => bool" ("_|-_~>_" [71,71,71] 70) "@widen" :: "prog => [ty , ty ] => bool" ("_|-_<=:_" [71,71,71] 70) "@narrow" :: "prog => [ty , ty ] => bool" ("_|-_:>_" [71,71,71] 70) "@cast" :: "prog => [ty , ty ] => bool" ("_|-_<=:? _"[71,71,71] 70) syntax (symbols) "@subint1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) "@subint" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) (* Defined in Decl.thy: \ "@subcls1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>C1_" [71,71,71] 70) "@subclseq":: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>C _" [71,71,71] 70) "@subcls" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>C _" [71,71,71] 70) *) "@implmt1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70) "@implmt" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70) "@widen" :: "prog => [ty , ty ] => bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70) "@narrow" :: "prog => [ty , ty ] => bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70) "@cast" :: "prog => [ty , ty ] => bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70) translations "G\<turnstile>I \<prec>I1 J" == "(I,J) ∈ subint1 G" "G\<turnstile>I \<preceq>I J" == "(I,J) ∈(subint1 G)^*" --{* cf. 9.1.3 *} (* Defined in Decl.thy: "G\<turnstile>C \<prec>C1 D" == "(C,D) ∈ subcls1 G" "G\<turnstile>C \<preceq>C D" == "(C,D) ∈(subcls1 G)^*" *) "G\<turnstile>C \<leadsto>1 I" == "(C,I) ∈ implmt1 G" "G\<turnstile>C \<leadsto> I" == "(C,I) ∈ implmt G" "G\<turnstile>S \<preceq> T" == "(S,T) ∈ widen G" "G\<turnstile>S \<succ> T" == "(S,T) ∈ narrow G" "G\<turnstile>S \<preceq>? T" == "(S,T) ∈ cast G" section "subclass and subinterface relations" (* direct subinterface in Decl.thy, cf. 9.1.3 *) (* direct subclass in Decl.thy, cf. 8.1.3 *) lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard] lemma subcls_direct1: "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<preceq>C D" apply (auto dest: subcls_direct) done lemma subcls1I1: "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<prec>C1 D" apply (auto dest: subcls1I) done lemma subcls_direct2: "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<prec>C D" apply (auto dest: subcls1I1) done lemma subclseq_trans: "[|G\<turnstile>A \<preceq>C B; G\<turnstile>B \<preceq>C C|] ==> G\<turnstile>A \<preceq>C C" by (blast intro: rtrancl_trans) lemma subcls_trans: "[|G\<turnstile>A \<prec>C B; G\<turnstile>B \<prec>C C|] ==> G\<turnstile>A \<prec>C C" by (blast intro: trancl_trans) lemma SXcpt_subcls_Throwable_lemma: "[|class G (SXcpt xn) = Some xc; super xc = (if xn = Throwable then Object else SXcpt Throwable)|] ==> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable" apply (case_tac "xn = Throwable") apply simp_all apply (drule subcls_direct) apply (auto dest: sym) done lemma subcls_ObjectI: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object" apply (erule ws_subcls1_induct) apply clarsimp apply (case_tac "C = Object") apply (fast intro: r_into_rtrancl [THEN rtrancl_trans])+ done lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>C C ==> C = Object" apply (erule rtrancl_induct) apply (auto dest: subcls1D) done lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>C C ==> False" apply (erule trancl_induct) apply (auto dest: subcls1D) done lemma subcls_ObjectI1 [intro!]: "[|C ≠ Object;is_class G C;ws_prog G|] ==> G\<turnstile>C \<prec>C Object" apply (drule (1) subcls_ObjectI) apply (auto intro: rtrancl_into_trancl3) done lemma subcls_is_class: "(C,D) ∈ (subcls1 G)^+ ==> is_class G C" apply (erule trancl_trans_induct) apply (auto dest!: subcls1D) done lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D ==> is_class G D --> is_class G C" apply (erule rtrancl_induct) apply (drule_tac [2] subcls1D) apply auto done lemma single_inheritance: "[|G\<turnstile>A \<prec>C1 B; G\<turnstile>A \<prec>C1 C|] ==> B = C" by (auto simp add: subcls1_def) lemma subcls_compareable: "[|G\<turnstile>A \<preceq>C X; G\<turnstile>A \<preceq>C Y |] ==> G\<turnstile>X \<preceq>C Y ∨ G\<turnstile>Y \<preceq>C X" by (rule triangle_lemma) (auto intro: single_inheritance) lemma subcls1_irrefl: "[|G\<turnstile>C \<prec>C1 D; ws_prog G |] ==> C ≠ D" proof assume ws: "ws_prog G" and subcls1: "G\<turnstile>C \<prec>C1 D" and eq_C_D: "C=D" from subcls1 obtain c where neq_C_Object: "C≠Object" and clsC: "class G C = Some c" and super_c: "super c = D" by (auto simp add: subcls1_def) with super_c subcls1 eq_C_D have subcls_super_c_C: "G\<turnstile>super c \<prec>C C" by auto from ws clsC neq_C_Object have "¬ G\<turnstile>super c \<prec>C C" by (auto dest: ws_prog_cdeclD) from this subcls_super_c_C show "False" by (rule notE) qed lemma no_subcls_Object: "G\<turnstile>C \<prec>C D ==> C ≠ Object" by (erule converse_trancl_induct) (auto dest: subcls1D) lemma subcls_acyclic: "[|G\<turnstile>C \<prec>C D; ws_prog G|] ==> ¬ G\<turnstile>D \<prec>C C" proof - assume ws: "ws_prog G" assume subcls_C_D: "G\<turnstile>C \<prec>C D" then show ?thesis proof (induct rule: converse_trancl_induct) fix C assume subcls1_C_D: "G\<turnstile>C \<prec>C1 D" then obtain c where "C≠Object" and "class G C = Some c" and "super c = D" by (auto simp add: subcls1_def) with ws show "¬ G\<turnstile>D \<prec>C C" by (auto dest: ws_prog_cdeclD) next fix C Z assume subcls1_C_Z: "G\<turnstile>C \<prec>C1 Z" and subcls_Z_D: "G\<turnstile>Z \<prec>C D" and nsubcls_D_Z: "¬ G\<turnstile>D \<prec>C Z" show "¬ G\<turnstile>D \<prec>C C" proof assume subcls_D_C: "G\<turnstile>D \<prec>C C" show "False" proof - from subcls_D_C subcls1_C_Z have "G\<turnstile>D \<prec>C Z" by (auto dest: r_into_trancl trancl_trans) with nsubcls_D_Z show ?thesis by (rule notE) qed qed qed qed lemma subclseq_cases [consumes 1, case_names Eq Subcls]: "[|G\<turnstile>C \<preceq>C D; C = D ==> P; G\<turnstile>C \<prec>C D ==> P|] ==> P" by (blast intro: rtrancl_cases) lemma subclseq_acyclic: "[|G\<turnstile>C \<preceq>C D; G\<turnstile>D \<preceq>C C; ws_prog G|] ==> C=D" by (auto elim: subclseq_cases dest: subcls_acyclic) lemma subcls_irrefl: "[|G\<turnstile>C \<prec>C D; ws_prog G|] ==> C ≠ D" proof - assume ws: "ws_prog G" assume subcls: "G\<turnstile>C \<prec>C D" then show ?thesis proof (induct rule: converse_trancl_induct) fix C assume "G\<turnstile>C \<prec>C1 D" with ws show "C≠D" by (blast dest: subcls1_irrefl) next fix C Z assume subcls1_C_Z: "G\<turnstile>C \<prec>C1 Z" and subcls_Z_D: "G\<turnstile>Z \<prec>C D" and neq_Z_D: "Z ≠ D" show "C≠D" proof assume eq_C_D: "C=D" show "False" proof - from subcls1_C_Z eq_C_D have "G\<turnstile>D \<prec>C Z" by (auto) also from subcls_Z_D ws have "¬ G\<turnstile>D \<prec>C Z" by (rule subcls_acyclic) ultimately show ?thesis by - (rule notE) qed qed qed qed lemma invert_subclseq: "[|G\<turnstile>C \<preceq>C D; ws_prog G|] ==> ¬ G\<turnstile>D \<prec>C C" proof - assume ws: "ws_prog G" and subclseq_C_D: "G\<turnstile>C \<preceq>C D" show ?thesis proof (cases "D=C") case True with ws show ?thesis by (auto dest: subcls_irrefl) next case False with subclseq_C_D have "G\<turnstile>C \<prec>C D" by (blast intro: rtrancl_into_trancl3) with ws show ?thesis by (blast dest: subcls_acyclic) qed qed lemma invert_subcls: "[|G\<turnstile>C \<prec>C D; ws_prog G|] ==> ¬ G\<turnstile>D \<preceq>C C" proof - assume ws: "ws_prog G" and subcls_C_D: "G\<turnstile>C \<prec>C D" then have nsubcls_D_C: "¬ G\<turnstile>D \<prec>C C" by (blast dest: subcls_acyclic) show ?thesis proof assume "G\<turnstile>D \<preceq>C C" then show "False" proof (cases rule: subclseq_cases) case Eq with ws subcls_C_D show ?thesis by (auto dest: subcls_irrefl) next case Subcls with nsubcls_D_C show ?thesis by blast qed qed qed lemma subcls_superD: "[|G\<turnstile>C \<prec>C D; class G C = Some c|] ==> G\<turnstile>(super c) \<preceq>C D" proof - assume clsC: "class G C = Some c" assume subcls_C_C: "G\<turnstile>C \<prec>C D" then obtain S where "G\<turnstile>C \<prec>C1 S" and subclseq_S_D: "G\<turnstile>S \<preceq>C D" by (blast dest: tranclD) with clsC have "S=super c" by (auto dest: subcls1D) with subclseq_S_D show ?thesis by simp qed lemma subclseq_superD: "[|G\<turnstile>C \<preceq>C D; C≠D;class G C = Some c|] ==> G\<turnstile>(super c) \<preceq>C D" proof - assume neq_C_D: "C≠D" assume clsC: "class G C = Some c" assume subclseq_C_D: "G\<turnstile>C \<preceq>C D" then show ?thesis proof (cases rule: subclseq_cases) case Eq with neq_C_D show ?thesis by contradiction next case Subcls with clsC show ?thesis by (blast dest: subcls_superD) qed qed section "implementation relation" defs --{* direct implementation, cf. 8.1.3 *} implmt1_def:"implmt1 G≡{(C,I). C≠Object ∧ (∃c∈class G C: I∈set (superIfs c))}" lemma implmt1D: "G\<turnstile>C\<leadsto>1I ==> C≠Object ∧ (∃c∈class G C: I∈set (superIfs c))" apply (unfold implmt1_def) apply auto done inductive "implmt G" intros --{* cf. 8.1.4 *} direct: "G\<turnstile>C\<leadsto>1J ==> G\<turnstile>C\<leadsto>J" subint: "[|G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J|] ==> G\<turnstile>C\<leadsto>J" subcls1: "[|G\<turnstile>C\<prec>C1D; G\<turnstile>D\<leadsto>J |] ==> G\<turnstile>C\<leadsto>J" lemma implmtD: "G\<turnstile>C\<leadsto>J ==> (∃I. G\<turnstile>C\<leadsto>1I ∧ G\<turnstile>I\<preceq>I J) ∨ (∃D. G\<turnstile>C\<prec>C1D ∧ G\<turnstile>D\<leadsto>J)" apply (erule implmt.induct) apply fast+ done lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I ==> R" by (auto dest!: implmtD implmt1D subcls1D) lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>C B ==> G\<turnstile>B\<leadsto>K --> G\<turnstile>A\<leadsto>K" apply (erule rtrancl_induct) apply (auto intro: implmt.subcls1) done lemma implmt_subint2: "[| G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K|] ==> G\<turnstile>A\<leadsto>K" apply (erule make_imp, erule implmt.induct) apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) done lemma implmt_is_class: "G\<turnstile>C\<leadsto>I ==> is_class G C" apply (erule implmt.induct) apply (blast dest: implmt1D subcls1D)+ done section "widening relation" inductive "widen G" intros --{*widening, viz. method invocation conversion, cf. 5.3 i.e. kind of syntactic subtyping *} refl: "G\<turnstile>T\<preceq>T" --{*identity conversion, cf. 5.1.1 *} subint: "G\<turnstile>I\<preceq>I J ==> G\<turnstile>Iface I\<preceq> Iface J" --{*wid.ref.conv.,cf. 5.1.4 *} int_obj: "G\<turnstile>Iface I\<preceq> Class Object" subcls: "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C\<preceq> Class D" implmt: "G\<turnstile>C\<leadsto>I ==> G\<turnstile>Class C\<preceq> Iface I" null: "G\<turnstile>NT\<preceq> RefT R" arr_obj: "G\<turnstile>T.[]\<preceq> Class Object" array: "G\<turnstile>RefT S\<preceq>RefT T ==> G\<turnstile>RefT S.[]\<preceq> RefT T.[]" declare widen.refl [intro!] declare widen.intros [simp] (* too strong in general: lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T ==> T = PrimT x" *) lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T ==> (∃y. T = PrimT y)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto (* too strong in general: lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x ==> S = PrimT x" *) lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x ==> ∃y. S = PrimT y" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto text {* These widening lemmata hold in Bali but are to strong for ordinary Java. They would not work for real Java Integral Types, like short, long, int. These lemmata are just for documentation and are not used. *} lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T ==> T = PrimT x" by (ind_cases "G\<turnstile>S\<preceq>T") simp_all lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x ==> S = PrimT x" by (ind_cases "G\<turnstile>S\<preceq>T") simp_all text {* Specialized versions for booleans also would work for real Java *} lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T ==> T = PrimT Boolean" by (ind_cases "G\<turnstile>S\<preceq>T") simp_all lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean ==> S = PrimT Boolean" by (ind_cases "G\<turnstile>S\<preceq>T") simp_all lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> ∃t. T=RefT t" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> ∃t. S=RefT t" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T ==> T=Class Object ∨ (∃J. T=Iface J)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J ==> S = NT ∨ (∃I. S = Iface I) ∨ (∃D. S = Class D)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J ==> G\<turnstile>I\<preceq>I J" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J" apply (rule iffI) apply (erule widen_Iface_Iface) apply (erule widen.subint) done lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> (∃D. T=Class D) ∨ (∃I. T=Iface I)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Class2: "G\<turnstile>S\<preceq> Class C ==> C = Object ∨ S = NT ∨ (∃D. S = Class D)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm ==> G\<turnstile>C\<preceq>C cm" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>C cm" apply (rule iffI) apply (erule widen_Class_Class) apply (erule widen.subcls) done lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I ==> G\<turnstile>C\<leadsto>I" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I" apply (rule iffI) apply (erule widen_Class_Iface) apply (erule widen.implmt) done lemma widen_Array: "G\<turnstile>S.[]\<preceq>T ==> T=Class Object ∨ (∃T'. T=T'.[] ∧ G\<turnstile>S\<preceq>T')" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] ==> S = NT ∨ (∃S'. S=S'.[] ∧ G\<turnstile>S'\<preceq>T)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T ==> T=Class Object ∨ T=PrimT t.[]" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_ArrayRefT: "G\<turnstile>RefT t.[]\<preceq>T ==> T=Class Object ∨ (∃s. T=RefT s.[] ∧ G\<turnstile>RefT t\<preceq>RefT s)" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_ArrayRefT_ArrayRefT_eq [simp]: "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'" apply (rule iffI) apply (drule widen_ArrayRefT) apply simp apply (erule widen.array) done lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] ==> G\<turnstile>T\<preceq>T'" apply (drule widen_Array) apply auto done lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C ==> C=Object" by (auto dest: widen_Array) lemma widen_NT2: "G\<turnstile>S\<preceq>NT ==> S = NT" apply (ind_cases "G\<turnstile>S\<preceq>T") by auto lemma widen_Object:"[|isrtype G T;ws_prog G|] ==> G\<turnstile>RefT T \<preceq> Class Object" apply (case_tac T) apply (auto) apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>C Object") apply (auto intro: subcls_ObjectI) done lemma widen_trans_lemma [rule_format (no_asm)]: "[|G\<turnstile>S\<preceq>U; ∀C. is_class G C --> G\<turnstile>C\<preceq>C Object|] ==> ∀T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T" apply (erule widen.induct) apply safe prefer 5 apply (drule widen_RefT) apply clarsimp apply (frule_tac [1] widen_Iface) apply (frule_tac [2] widen_Class) apply (frule_tac [3] widen_Class) apply (frule_tac [4] widen_Iface) apply (frule_tac [5] widen_Class) apply (frule_tac [6] widen_Array) apply safe apply (rule widen.int_obj) prefer 6 apply (drule implmt_is_class) apply simp apply (tactic "ALLGOALS (etac thin_rl)") prefer 6 apply simp apply (rule_tac [9] widen.arr_obj) apply (rotate_tac [9] -1) apply (frule_tac [9] widen_RefT) apply (auto elim!: rtrancl_trans subcls_implmt implmt_subint2) done lemma ws_widen_trans: "[|G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G|] ==> G\<turnstile>S\<preceq>T" by (auto intro: widen_trans_lemma subcls_ObjectI) lemma widen_antisym_lemma [rule_format (no_asm)]: "[|G\<turnstile>S\<preceq>T; ∀I J. G\<turnstile>I\<preceq>I J ∧ G\<turnstile>J\<preceq>I I --> I = J; ∀C D. G\<turnstile>C\<preceq>C D ∧ G\<turnstile>D\<preceq>C C --> C = D; ∀I . G\<turnstile>Object\<leadsto>I --> False|] ==> G\<turnstile>T\<preceq>S --> S = T" apply (erule widen.induct) apply (auto dest: widen_Iface widen_NT2 widen_Class) done lemmas subint_antisym = subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] lemmas subcls_antisym = subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] lemma widen_antisym: "[|G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G|] ==> S=T" by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] subcls_antisym [THEN antisymD]) lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T ==> T=Class Object" apply (frule widen_Class) apply (fast dest: widen_Class_Class widen_Class_Iface) done constdefs widens :: "prog => [ty list, ty list] => bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) "G\<turnstile>Ts[\<preceq>]Ts' ≡ list_all2 (λT T'. G\<turnstile>T\<preceq>T') Ts Ts'" lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]" apply (unfold widens_def) apply auto done lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T ∧ G\<turnstile>Ss[\<preceq>]Ts)" apply (unfold widens_def) apply auto done section "narrowing relation" (* all properties of narrowing and casting conversions we actually need *) (* these can easily be proven from the definitions below *) (* rules cast_RefT2 "G\<turnstile>S\<preceq>? RefT R ==> ∃t. S=RefT t" cast_PrimT2 "G\<turnstile>S\<preceq>? PrimT pt ==> ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt" *) (* more detailed than necessary for type-safety, see above rules. *) inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *) subcls: "G\<turnstile>C\<preceq>C D ==> G\<turnstile> Class D\<succ>Class C" implmt: "¬G\<turnstile>C\<leadsto>I ==> G\<turnstile> Class C\<succ>Iface I" obj_arr: "G\<turnstile>Class Object\<succ>T.[]" int_cls: "G\<turnstile> Iface I\<succ>Class C" subint: "imethds G I hidings imethds G J entails (λ(md, mh ) (md',mh'). G\<turnstile>mrt mh\<preceq>mrt mh') ==> ¬G\<turnstile>I\<preceq>I J ==> G\<turnstile> Iface I\<succ>Iface J" array: "G\<turnstile>RefT S\<succ>RefT T ==> G\<turnstile> RefT S.[]\<succ>RefT T.[]" (*unused*) lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T ==> ∃t. T=RefT t" apply (ind_cases "G\<turnstile>S\<succ>T") by auto lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R ==> ∃t. S=RefT t" apply (ind_cases "G\<turnstile>S\<succ>T") by auto (*unused*) lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T ==> ∃t. T=PrimT t" apply (ind_cases "G\<turnstile>S\<succ>T") by auto lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt ==> ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt" apply (ind_cases "G\<turnstile>S\<succ>T") by auto text {* These narrowing lemmata hold in Bali but are to strong for ordinary Java. They would not work for real Java Integral Types, like short, long, int. These lemmata are just for documentation and are not used. *} lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T ==> T=PrimT pt" by (ind_cases "G\<turnstile>S\<succ>T") simp_all lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt ==> S=PrimT pt" by (ind_cases "G\<turnstile>S\<succ>T") simp_all text {* Specialized versions for booleans also would work for real Java *} lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T ==> T=PrimT Boolean" by (ind_cases "G\<turnstile>S\<succ>T") simp_all lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean ==> S=PrimT Boolean" by (ind_cases "G\<turnstile>S\<succ>T") simp_all section "casting relation" inductive "cast G" intros --{* casting conversion, cf. 5.5 *} widen: "G\<turnstile>S\<preceq>T ==> G\<turnstile>S\<preceq>? T" narrow: "G\<turnstile>S\<succ>T ==> G\<turnstile>S\<preceq>? T" (*unused*) lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T ==> ∃t. T=RefT t" apply (ind_cases "G\<turnstile>S\<preceq>? T") by (auto dest: widen_RefT narrow_RefT) lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R ==> ∃t. S=RefT t" apply (ind_cases "G\<turnstile>S\<preceq>? T") by (auto dest: widen_RefT2 narrow_RefT2) (*unused*) lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T ==> ∃t. T=PrimT t" apply (ind_cases "G\<turnstile>S\<preceq>? T") by (auto dest: widen_PrimT narrow_PrimT) lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt ==> ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt" apply (ind_cases "G\<turnstile>S\<preceq>? T") by (auto dest: widen_PrimT2 narrow_PrimT2) lemma cast_Boolean: assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T" shows "T=PrimT Boolean" using bool_cast proof (cases) case widen hence "G\<turnstile>PrimT Boolean\<preceq> T" by simp thus ?thesis by (rule widen_Boolean) next case narrow hence "G\<turnstile>PrimT Boolean\<succ>T" by simp thus ?thesis by (rule narrow_Boolean) qed lemma cast_Boolean2: assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean" shows "S = PrimT Boolean" using bool_cast proof (cases) case widen hence "G\<turnstile>S\<preceq> PrimT Boolean" by simp thus ?thesis by (rule widen_Boolean2) next case narrow hence "G\<turnstile>S\<succ>PrimT Boolean" by simp thus ?thesis by (rule narrow_Boolean2) qed end
lemmas subcls_direct:
[| class G C = Some c; C ≠ Object |] ==> G|-C<=:C super c
lemmas subcls_direct:
[| class G C = Some c; C ≠ Object |] ==> G|-C<=:C super c
lemma subcls_direct1:
[| class G C = Some c; C ≠ Object; D = super c |] ==> G|-C<=:C D
lemma subcls1I1:
[| class G C = Some c; C ≠ Object; D = super c |] ==> G|-C<:C1D
lemma subcls_direct2:
[| class G C = Some c; C ≠ Object; D = super c |] ==> G|-C<:C D
lemma subclseq_trans:
[| G|-A<=:C B; G|-B<=:C C |] ==> G|-A<=:C C
lemma subcls_trans:
[| G|-A<:C B; G|-B<:C C |] ==> G|-A<:C C
lemma SXcpt_subcls_Throwable_lemma:
[| class G (SXcpt xn) = Some xc; super xc = (if xn = Throwable then Object else SXcpt Throwable) |] ==> G|-SXcpt xn<=:C SXcpt Throwable
lemma subcls_ObjectI:
[| is_class G C; ws_prog G |] ==> G|-C<=:C Object
lemma subclseq_ObjectD:
G|-Object<=:C C ==> C = Object
lemma subcls_ObjectD:
G|-Object<:C C ==> False
lemma subcls_ObjectI1:
[| C ≠ Object; is_class G C; ws_prog G |] ==> G|-C<:C Object
lemma subcls_is_class:
G|-C<:C D ==> is_class G C
lemma subcls_is_class2:
[| G|-C<=:C D; is_class G D |] ==> is_class G C
lemma single_inheritance:
[| G|-A<:C1B; G|-A<:C1C |] ==> B = C
lemma subcls_compareable:
[| G|-A<=:C X; G|-A<=:C Y |] ==> G|-X<=:C Y ∨ G|-Y<=:C X
lemma subcls1_irrefl:
[| G|-C<:C1D; ws_prog G |] ==> C ≠ D
lemma no_subcls_Object:
G|-C<:C D ==> C ≠ Object
lemma subcls_acyclic:
[| G|-C<:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)+
lemma subclseq_cases:
[| G|-C<=:C D; C = D ==> P; G|-C<:C D ==> P |] ==> P
lemma subclseq_acyclic:
[| G|-C<=:C D; G|-D<=:C C; ws_prog G |] ==> C = D
lemma subcls_irrefl:
[| G|-C<:C D; ws_prog G |] ==> C ≠ D
lemma invert_subclseq:
[| G|-C<=:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)+
lemma invert_subcls:
[| G|-C<:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)*
lemma subcls_superD:
[| G|-C<:C D; class G C = Some c |] ==> G|-super c<=:C D
lemma subclseq_superD:
[| G|-C<=:C D; C ≠ D; class G C = Some c |] ==> G|-super c<=:C D
lemma implmt1D:
G|-C~>1I ==> C ≠ Object ∧ (? c:class G C: I ∈ set (superIfs c))
lemma implmtD:
G|-C~>J ==> (∃I. G|-C~>1I ∧ G|-I<=:I J) ∨ (∃D. G|-C<:C1D ∧ G|-D~>J)
lemma implmt_ObjectE:
G|-Object~>I ==> R
lemma subcls_implmt:
[| G|-A<=:C B; G|-B~>K |] ==> G|-A~>K
lemma implmt_subint2:
[| G|-A~>J; G|-J<=:I K |] ==> G|-A~>K
lemma implmt_is_class:
G|-C~>I ==> is_class G C
lemma widen_PrimT:
G|-PrimT x<=:T ==> ∃y. T = PrimT y
lemma widen_PrimT2:
G|-S<=:PrimT x ==> ∃y. S = PrimT y
lemma widen_PrimT_strong:
G|-PrimT x<=:T ==> T = PrimT x
lemma widen_PrimT2_strong:
G|-S<=:PrimT x ==> S = PrimT x
lemma widen_Boolean:
G|-PrimT Boolean<=:T ==> T = PrimT Boolean
lemma widen_Boolean2:
G|-S<=:PrimT Boolean ==> S = PrimT Boolean
lemma widen_RefT:
G|-RefT R<=:T ==> ∃t. T = RefT t
lemma widen_RefT2:
G|-S<=:RefT R ==> ∃t. S = RefT t
lemma widen_Iface:
G|-Iface I<=:T ==> T = Class Object ∨ (∃J. T = Iface J)
lemma widen_Iface2:
G|-S<=:Iface J ==> S = NT ∨ (∃I. S = Iface I) ∨ (∃D. S = Class D)
lemma widen_Iface_Iface:
G|-Iface I<=:Iface J ==> G|-I<=:I J
lemma widen_Iface_Iface_eq:
G|-Iface I<=:Iface J = G|-I<=:I J
lemma widen_Class:
G|-Class C<=:T ==> (∃D. T = Class D) ∨ (∃I. T = Iface I)
lemma widen_Class2:
G|-S<=:Class C ==> C = Object ∨ S = NT ∨ (∃D. S = Class D)
lemma widen_Class_Class:
G|-Class C<=:Class cm ==> G|-C<=:C cm
lemma widen_Class_Class_eq:
G|-Class C<=:Class cm = G|-C<=:C cm
lemma widen_Class_Iface:
G|-Class C<=:Iface I ==> G|-C~>I
lemma widen_Class_Iface_eq:
G|-Class C<=:Iface I = G|-C~>I
lemma widen_Array:
G|-S.[]<=:T ==> T = Class Object ∨ (∃T'. T = T'.[] ∧ G|-S<=:T')
lemma widen_Array2:
G|-S<=:T.[] ==> S = NT ∨ (∃S'. S = S'.[] ∧ G|-S'<=:T)
lemma widen_ArrayPrimT:
G|-PrimT t.[]<=:T ==> T = Class Object ∨ T = PrimT t.[]
lemma widen_ArrayRefT:
G|-RefT t.[]<=:T ==> T = Class Object ∨ (∃s. T = RefT s.[] ∧ G|-RefT t<=:RefT s)
lemma widen_ArrayRefT_ArrayRefT_eq:
G|-RefT T.[]<=:RefT T'.[] = G|-RefT T<=:RefT T'
lemma widen_Array_Array:
G|-T.[]<=:T'.[] ==> G|-T<=:T'
lemma widen_Array_Class:
G|-S.[]<=:Class C ==> C = Object
lemma widen_NT2:
G|-S<=:NT ==> S = NT
lemma widen_Object:
[| isrtype G T; ws_prog G |] ==> G|-RefT T<=:Class Object
lemma widen_trans_lemma:
[| G|-S<=:U; ∀C. is_class G C --> G|-C<=:C Object; G|-U<=:T |] ==> G|-S<=:T
lemma ws_widen_trans:
[| G|-S<=:U; G|-U<=:T; ws_prog G |] ==> G|-S<=:T
lemma widen_antisym_lemma:
[| G|-S<=:T; ∀I J. G|-I<=:I J ∧ G|-J<=:I I --> I = J; ∀C D. G|-C<=:C D ∧ G|-D<=:C C --> C = D; ∀I. G|-Object~>I --> False; G|-T<=:S |] ==> S = T
lemmas subint_antisym:
ws_prog G ==> antisym ((subint1 G)*)
lemmas subint_antisym:
ws_prog G ==> antisym ((subint1 G)*)
lemmas subcls_antisym:
ws_prog G ==> antisym ((subcls1 G)*)
lemmas subcls_antisym:
ws_prog G ==> antisym ((subcls1 G)*)
lemma widen_antisym:
[| G|-S<=:T; G|-T<=:S; ws_prog G |] ==> S = T
lemma widen_ObjectD:
G|-Class Object<=:T ==> T = Class Object
lemma widens_Nil:
G\<turnstile>[][\<preceq>][]
lemma widens_Cons:
G\<turnstile>(S # Ss)[\<preceq>](T # Ts) = (G|-S<=:T ∧ G\<turnstile>Ss[\<preceq>]Ts)
lemma narrow_RefT:
G|-RefT R:>T ==> ∃t. T = RefT t
lemma narrow_RefT2:
G|-S:>RefT R ==> ∃t. S = RefT t
lemma narrow_PrimT:
G|-PrimT pt:>T ==> ∃t. T = PrimT t
lemma narrow_PrimT2:
G|-S:>PrimT pt ==> ∃t. S = PrimT t ∧ G|-PrimT t<=:PrimT pt
lemma narrow_PrimT_strong:
G|-PrimT pt:>T ==> T = PrimT pt
lemma narrow_PrimT2_strong:
G|-S:>PrimT pt ==> S = PrimT pt
lemma narrow_Boolean:
G|-PrimT Boolean:>T ==> T = PrimT Boolean
lemma narrow_Boolean2:
G|-S:>PrimT Boolean ==> S = PrimT Boolean
lemma cast_RefT:
G|-RefT R<=:? T ==> ∃t. T = RefT t
lemma cast_RefT2:
G|-S<=:? RefT R ==> ∃t. S = RefT t
lemma cast_PrimT:
G|-PrimT pt<=:? T ==> ∃t. T = PrimT t
lemma cast_PrimT2:
G|-S<=:? PrimT pt ==> ∃t. S = PrimT t ∧ G|-PrimT t<=:PrimT pt
lemma cast_Boolean:
G|-PrimT Boolean<=:? T ==> T = PrimT Boolean
lemma cast_Boolean2:
G|-S<=:? PrimT Boolean ==> S = PrimT Boolean