12857

1 
(* Title: HOL/Bali/TypeRel.thy

12854

2 
ID: $Id$


3 
Author: David von Oheimb

12858

4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

12854

5 
*)


6 
header {* The relations between Java types *}


7 


8 
theory TypeRel = Decl:


9 


10 
text {*


11 
simplifications:


12 
\begin{itemize}


13 
\item subinterface, subclass and widening relation includes identity


14 
\end{itemize}


15 
improvements over Java Specification 1.0:


16 
\begin{itemize}


17 
\item narrowing reference conversion also in cases where the return types of a


18 
pair of methods common to both types are in widening (rather identity)


19 
relation


20 
\item one could add similar constraints also for other cases


21 
\end{itemize}


22 
design issues:


23 
\begin{itemize}


24 
\item the type relations do not require @{text is_type} for their arguments


25 
\item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class}


26 
for their first arguments, which is required for their finiteness


27 
\end{itemize}


28 
*}


29 


30 
consts


31 


32 
(*subint1, in Decl.thy*) (* direct subinterface *)


33 
(*subint , by translation*) (* subinterface (+ identity) *)


34 
(*subcls1, in Decl.thy*) (* direct subclass *)


35 
(*subcls , by translation*) (* subclass *)


36 
(*subclseq, by translation*) (* subclass + identity *)


37 
implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" (* direct implementation *)


38 
implmt :: "prog \<Rightarrow> (qtname \<times> qtname) set" (* implementation *)


39 
widen :: "prog \<Rightarrow> (ty \<times> ty ) set" (* widening *)


40 
narrow :: "prog \<Rightarrow> (ty \<times> ty ) set" (* narrowing *)


41 
cast :: "prog \<Rightarrow> (ty \<times> ty ) set" (* casting *)


42 


43 
syntax


44 


45 
"@subint1" :: "prog => [qtname, qtname] => bool" ("__<:I1_" [71,71,71] 70)


46 
"@subint" :: "prog => [qtname, qtname] => bool" ("__<=:I _"[71,71,71] 70)


47 
(* Defined in Decl.thy:


48 
"@subcls1" :: "prog => [qtname, qtname] => bool" ("__<:C1_" [71,71,71] 70)


49 
"@subclseq":: "prog => [qtname, qtname] => bool" ("__<=:C _"[71,71,71] 70)


50 
"@subcls" :: "prog => [qtname, qtname] => bool" ("__<:C _"[71,71,71] 70)


51 
*)


52 
"@implmt1" :: "prog => [qtname, qtname] => bool" ("__~>1_" [71,71,71] 70)


53 
"@implmt" :: "prog => [qtname, qtname] => bool" ("__~>_" [71,71,71] 70)


54 
"@widen" :: "prog => [ty , ty ] => bool" ("__<=:_" [71,71,71] 70)


55 
"@narrow" :: "prog => [ty , ty ] => bool" ("__:>_" [71,71,71] 70)


56 
"@cast" :: "prog => [ty , ty ] => bool" ("__<=:? _"[71,71,71] 70)


57 


58 
syntax (symbols)


59 


60 
"@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)


61 
"@subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)


62 
(* Defined in Decl.thy:


63 
\ "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70)


64 
"@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70)


65 
"@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70)


66 
*)


67 
"@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)


68 
"@implmt" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)


69 
"@widen" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)


70 
"@narrow" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)


71 
"@cast" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)


72 


73 
translations


74 


75 
"G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"


76 
"G\<turnstile>I \<preceq>I J" == "(I,J) \<in>(subint1 G)^*" (* cf. 9.1.3 *)


77 
(* Defined in Decl.thy:


78 
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"


79 
"G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*"


80 
*)


81 
"G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"


82 
"G\<turnstile>C \<leadsto> I" == "(C,I) \<in> implmt G"


83 
"G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G"


84 
"G\<turnstile>S \<succ> T" == "(S,T) \<in> narrow G"


85 
"G\<turnstile>S \<preceq>? T" == "(S,T) \<in> cast G"


86 


87 


88 
section "subclass and subinterface relations"


89 


90 
(* direct subinterface in Decl.thy, cf. 9.1.3 *)


91 
(* direct subclass in Decl.thy, cf. 8.1.3 *)


92 


93 
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]


94 


95 
lemma subcls_direct1:


96 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"


97 
apply (auto dest: subcls_direct)


98 
done


99 


100 
lemma subcls1I1:


101 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C\<^sub>1 D"


102 
apply (auto dest: subcls1I)


103 
done


104 


105 
lemma subcls_direct2:


106 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C D"


107 
apply (auto dest: subcls1I1)


108 
done


109 


110 
lemma subclseq_trans: "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C B; G\<turnstile>B \<preceq>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<preceq>\<^sub>C C"


111 
by (blast intro: rtrancl_trans)


112 


113 
lemma subcls_trans: "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C B; G\<turnstile>B \<prec>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<prec>\<^sub>C C"


114 
by (blast intro: trancl_trans)


115 


116 
lemma SXcpt_subcls_Throwable_lemma:


117 
"\<lbrakk>class G (SXcpt xn) = Some xc;


118 
super xc = (if xn = Throwable then Object else SXcpt Throwable)\<rbrakk>


119 
\<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"


120 
apply (case_tac "xn = Throwable")


121 
apply simp_all


122 
apply (drule subcls_direct)


123 
apply (auto dest: sym)


124 
done


125 


126 
lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object"


127 
apply (erule ws_subcls1_induct)


128 
apply clarsimp


129 
apply (case_tac "C = Object")


130 
apply (fast intro: r_into_rtrancl [THEN rtrancl_trans])+


131 
done


132 


133 
lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>\<^sub>C C \<Longrightarrow> C = Object"


134 
apply (erule rtrancl_induct)


135 
apply (auto dest: subcls1D)


136 
done


137 


138 
lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>\<^sub>C C \<Longrightarrow> False"


139 
apply (erule trancl_induct)


140 
apply (auto dest: subcls1D)


141 
done


142 


143 
lemma subcls_ObjectI1 [intro!]:


144 
"\<lbrakk>C \<noteq> Object;is_class G C;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C \<prec>\<^sub>C Object"


145 
apply (drule (1) subcls_ObjectI)


146 
apply (auto intro: rtrancl_into_trancl3)


147 
done


148 


149 
lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C"


150 
apply (erule trancl_trans_induct)


151 
apply (auto dest!: subcls1D)


152 
done


153 


154 
lemma subcls_is_class2 [rule_format (no_asm)]:


155 
"G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"


156 
apply (erule rtrancl_induct)


157 
apply (drule_tac [2] subcls1D)


158 
apply auto


159 
done


160 


161 
lemma single_inheritance:


162 
"\<lbrakk>G\<turnstile>A \<prec>\<^sub>C\<^sub>1 B; G\<turnstile>A \<prec>\<^sub>C\<^sub>1 C\<rbrakk> \<Longrightarrow> B = C"


163 
by (auto simp add: subcls1_def)


164 


165 
lemma subcls_compareable:


166 
"\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C X; G\<turnstile>A \<preceq>\<^sub>C Y


167 
\<rbrakk> \<Longrightarrow> G\<turnstile>X \<preceq>\<^sub>C Y \<or> G\<turnstile>Y \<preceq>\<^sub>C X"


168 
by (rule triangle_lemma) (auto intro: single_inheritance)


169 


170 
lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D; ws_prog G \<rbrakk>


171 
\<Longrightarrow> C \<noteq> D"


172 
proof


173 
assume ws: "ws_prog G" and


174 
subcls1: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" and


175 
eq_C_D: "C=D"


176 
from subcls1 obtain c


177 
where


178 
neq_C_Object: "C\<noteq>Object" and


179 
clsC: "class G C = Some c" and


180 
super_c: "super c = D"


181 
by (auto simp add: subcls1_def)


182 
with super_c subcls1 eq_C_D


183 
have subcls_super_c_C: "G\<turnstile>super c \<prec>\<^sub>C C"


184 
by auto


185 
from ws clsC neq_C_Object


186 
have "\<not> G\<turnstile>super c \<prec>\<^sub>C C"


187 
by (auto dest: ws_prog_cdeclD)


188 
from this subcls_super_c_C


189 
show "False"


190 
by (rule notE)


191 
qed


192 


193 
lemma no_subcls_Object: "G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> C \<noteq> Object"


194 
by (erule converse_trancl_induct) (auto dest: subcls1D)


195 


196 
lemma subcls_acyclic: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"


197 
proof 


198 
assume ws: "ws_prog G"


199 
assume subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"


200 
then show ?thesis


201 
proof (induct rule: converse_trancl_induct)


202 
fix C


203 
assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D"


204 
then obtain c where


205 
"C\<noteq>Object" and


206 
"class G C = Some c" and


207 
"super c = D"


208 
by (auto simp add: subcls1_def)


209 
with ws


210 
show "\<not> G\<turnstile>D \<prec>\<^sub>C C"


211 
by (auto dest: ws_prog_cdeclD)


212 
next


213 
fix C Z


214 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and


215 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and


216 
nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z"


217 
show "\<not> G\<turnstile>D \<prec>\<^sub>C C"


218 
proof


219 
assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C"


220 
show "False"


221 
proof 


222 
from subcls_D_C subcls1_C_Z


223 
have "G\<turnstile>D \<prec>\<^sub>C Z"


224 
by (auto dest: r_into_trancl trancl_trans)


225 
with nsubcls_D_Z


226 
show ?thesis


227 
by (rule notE)


228 
qed


229 
qed


230 
qed


231 
qed


232 


233 
lemma subclseq_cases [consumes 1, case_names Eq Subcls]:


234 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"


235 
by (blast intro: rtrancl_cases)


236 


237 
lemma subclseq_acyclic:


238 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"


239 
by (auto elim: subclseq_cases dest: subcls_acyclic)


240 


241 
lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>


242 
\<Longrightarrow> C \<noteq> D"


243 
proof 


244 
assume ws: "ws_prog G"


245 
assume subcls: "G\<turnstile>C \<prec>\<^sub>C D"


246 
then show ?thesis


247 
proof (induct rule: converse_trancl_induct)


248 
fix C


249 
assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D"


250 
with ws


251 
show "C\<noteq>D"


252 
by (blast dest: subcls1_irrefl)


253 
next


254 
fix C Z


255 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and


256 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and


257 
neq_Z_D: "Z \<noteq> D"


258 
show "C\<noteq>D"


259 
proof


260 
assume eq_C_D: "C=D"


261 
show "False"


262 
proof 


263 
from subcls1_C_Z eq_C_D


264 
have "G\<turnstile>D \<prec>\<^sub>C Z"


265 
by (auto)


266 
also


267 
from subcls_Z_D ws


268 
have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"


269 
by (rule subcls_acyclic)


270 
ultimately


271 
show ?thesis


272 
by  (rule notE)


273 
qed


274 
qed


275 
qed


276 
qed


277 


278 
lemma invert_subclseq:


279 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk>


280 
\<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"


281 
proof 


282 
assume ws: "ws_prog G" and


283 
subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"


284 
show ?thesis


285 
proof (cases "D=C")


286 
case True


287 
with ws


288 
show ?thesis


289 
by (auto dest: subcls_irrefl)


290 
next


291 
case False


292 
with subclseq_C_D


293 
have "G\<turnstile>C \<prec>\<^sub>C D"


294 
by (blast intro: rtrancl_into_trancl3)


295 
with ws


296 
show ?thesis


297 
by (blast dest: subcls_acyclic)


298 
qed


299 
qed


300 


301 
lemma invert_subcls:


302 
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>


303 
\<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C"


304 
proof 


305 
assume ws: "ws_prog G" and


306 
subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"


307 
then


308 
have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C"


309 
by (blast dest: subcls_acyclic)


310 
show ?thesis


311 
proof


312 
assume "G\<turnstile>D \<preceq>\<^sub>C C"


313 
then show "False"


314 
proof (cases rule: subclseq_cases)


315 
case Eq


316 
with ws subcls_C_D


317 
show ?thesis


318 
by (auto dest: subcls_irrefl)


319 
next


320 
case Subcls


321 
with nsubcls_D_C


322 
show ?thesis


323 
by blast


324 
qed


325 
qed


326 
qed


327 


328 
lemma subcls_superD:


329 
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"


330 
proof 


331 
assume clsC: "class G C = Some c"


332 
assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D"


333 
then obtain S where


334 
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" and


335 
subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D"


336 
by (blast dest: tranclD)


337 
with clsC


338 
have "S=super c"


339 
by (auto dest: subcls1D)


340 
with subclseq_S_D show ?thesis by simp


341 
qed


342 


343 


344 
lemma subclseq_superD:


345 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C\<noteq>D;class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"


346 
proof 


347 
assume neq_C_D: "C\<noteq>D"


348 
assume clsC: "class G C = Some c"


349 
assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"


350 
then show ?thesis


351 
proof (cases rule: subclseq_cases)


352 
case Eq with neq_C_D show ?thesis by contradiction


353 
next


354 
case Subcls


355 
with clsC show ?thesis by (blast dest: subcls_superD)


356 
qed


357 
qed


358 


359 
section "implementation relation"


360 


361 
defs


362 
(* direct implementation, cf. 8.1.3 *)


363 
implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"


364 


365 
lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"


366 
apply (unfold implmt1_def)


367 
apply auto


368 
done


369 


370 


371 
inductive "implmt G" intros (* cf. 8.1.4 *)


372 


373 
direct: "G\<turnstile>C\<leadsto>1J \<spacespace>\<spacespace> \<Longrightarrow> G\<turnstile>C\<leadsto>J"


374 
subint: "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J"


375 
subcls1: "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C\<^sub>1D; G\<turnstile>D\<leadsto>J \<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J"


376 


377 
lemma implmtD: "G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> (\<exists>D. G\<turnstile>C\<prec>\<^sub>C\<^sub>1D \<and> G\<turnstile>D\<leadsto>J)"


378 
apply (erule implmt.induct)


379 
apply fast+


380 
done


381 


382 
lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"


383 
by (auto dest!: implmtD implmt1D subcls1D)


384 


385 
lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>\<^sub>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K"


386 
apply (erule rtrancl_induct)


387 
apply (auto intro: implmt.subcls1)


388 
done


389 


390 
lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"


391 
apply (erule make_imp, erule implmt.induct)


392 
apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)


393 
done


394 


395 
lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"


396 
apply (erule implmt.induct)


397 
apply (blast dest: implmt1D subcls1D)+


398 
done


399 


400 


401 
section "widening relation"


402 


403 
inductive "widen G" intros(*widening, viz. method invocation conversion, cf. 5.3


404 
i.e. kind of syntactic subtyping *)


405 
refl: "G\<turnstile>T\<preceq>T"(*identity conversion, cf. 5.1.1 *)


406 
subint: "G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J"(*wid.ref.conv.,cf. 5.1.4 *)


407 
int_obj: "G\<turnstile>Iface I\<preceq> Class Object"


408 
subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D"


409 
implmt: "G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I"


410 
null: "G\<turnstile>NT\<preceq> RefT R"


411 
arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"


412 
array: "G\<turnstile>RefT S\<preceq>RefT T \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"


413 


414 
declare widen.refl [intro!]


415 
declare widen.intros [simp]


416 


417 
(* too strong in general:


418 
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"


419 
*)


420 
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"


421 
apply (ind_cases "G\<turnstile>S\<preceq>T")


422 
by auto


423 


424 
(* too strong in general:


425 
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"


426 
*)


427 
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"


428 
apply (ind_cases "G\<turnstile>S\<preceq>T")


429 
by auto


430 


431 
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"


432 
apply (ind_cases "G\<turnstile>S\<preceq>T")


433 
by auto


434 


435 
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"


436 
apply (ind_cases "G\<turnstile>S\<preceq>T")


437 
by auto


438 


439 
lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"


440 
apply (ind_cases "G\<turnstile>S\<preceq>T")


441 
by auto


442 


443 
lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"


444 
apply (ind_cases "G\<turnstile>S\<preceq>T")


445 
by auto


446 


447 
lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"


448 
apply (ind_cases "G\<turnstile>S\<preceq>T")


449 
by auto


450 


451 
lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"


452 
apply (rule iffI)


453 
apply (erule widen_Iface_Iface)


454 
apply (erule widen.subint)


455 
done


456 


457 
lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow> (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"


458 
apply (ind_cases "G\<turnstile>S\<preceq>T")


459 
by auto


460 


461 
lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"


462 
apply (ind_cases "G\<turnstile>S\<preceq>T")


463 
by auto


464 


465 
lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"


466 
apply (ind_cases "G\<turnstile>S\<preceq>T")


467 
by auto


468 


469 
lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"


470 
apply (rule iffI)


471 
apply (erule widen_Class_Class)


472 
apply (erule widen.subcls)


473 
done


474 


475 
lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"


476 
apply (ind_cases "G\<turnstile>S\<preceq>T")


477 
by auto


478 


479 
lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"


480 
apply (rule iffI)


481 
apply (erule widen_Class_Iface)


482 
apply (erule widen.implmt)


483 
done


484 


485 
lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"


486 
apply (ind_cases "G\<turnstile>S\<preceq>T")


487 
by auto


488 


489 
lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"


490 
apply (ind_cases "G\<turnstile>S\<preceq>T")


491 
by auto


492 


493 


494 
lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"


495 
apply (ind_cases "G\<turnstile>S\<preceq>T")


496 
by auto


497 


498 
lemma widen_ArrayRefT:


499 
"G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"


500 
apply (ind_cases "G\<turnstile>S\<preceq>T")


501 
by auto


502 


503 
lemma widen_ArrayRefT_ArrayRefT_eq [simp]:


504 
"G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"


505 
apply (rule iffI)


506 
apply (drule widen_ArrayRefT)


507 
apply simp


508 
apply (erule widen.array)


509 
done


510 


511 
lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"


512 
apply (drule widen_Array)


513 
apply auto


514 
done


515 


516 
lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object"


517 
by (auto dest: widen_Array)


518 


519 
(*


520 
qed_typerel "widen_NT2" "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"


521 
[prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = NT \<longrightarrow> S = NT"]


522 
*)


523 
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"


524 
apply (ind_cases "G\<turnstile>S\<preceq>T")


525 
by auto


526 


527 
lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"


528 
apply (case_tac T)


529 
apply (auto)


530 
apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object")


531 
apply (auto intro: subcls_ObjectI)


532 
done


533 


534 
lemma widen_trans_lemma [rule_format (no_asm)]:


535 
"\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T"


536 
apply (erule widen.induct)


537 
apply safe


538 
prefer 5 apply (drule widen_RefT) apply clarsimp


539 
apply (frule_tac [1] widen_Iface)


540 
apply (frule_tac [2] widen_Class)


541 
apply (frule_tac [3] widen_Class)


542 
apply (frule_tac [4] widen_Iface)


543 
apply (frule_tac [5] widen_Class)


544 
apply (frule_tac [6] widen_Array)


545 
apply safe


546 
apply (rule widen.int_obj)


547 
prefer 6 apply (drule implmt_is_class) apply simp


548 
apply (tactic "ALLGOALS (etac thin_rl)")


549 
prefer 6 apply simp


550 
apply (rule_tac [9] widen.arr_obj)


551 
apply (rotate_tac [9] 1)


552 
apply (frule_tac [9] widen_RefT)


553 
apply (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)


554 
done


555 


556 
lemma ws_widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"


557 
by (auto intro: widen_trans_lemma subcls_ObjectI)


558 


559 
lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;


560 
\<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;


561 
\<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D;


562 
\<forall>I . G\<turnstile>Object\<leadsto>I \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T"


563 
apply (erule widen.induct)


564 
apply (auto dest: widen_Iface widen_NT2 widen_Class)


565 
done


566 


567 
lemmas subint_antisym =


568 
subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]


569 
lemmas subcls_antisym =


570 
subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]


571 


572 
lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"


573 
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD]


574 
subcls_antisym [THEN antisymD])


575 


576 
lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"


577 
apply (frule widen_Class)


578 
apply (fast dest: widen_Class_Class widen_Class_Iface)


579 
done


580 


581 
constdefs


582 
widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)


583 
"G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"


584 


585 
lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"


586 
apply (unfold widens_def)


587 
apply auto


588 
done


589 


590 
lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)"


591 
apply (unfold widens_def)


592 
apply auto


593 
done


594 


595 


596 
section "narrowing relation"


597 


598 
(* all properties of narrowing and casting conversions we actually need *)


599 
(* these can easily be proven from the definitions below *)


600 
(*


601 
rules


602 
cast_RefT2 "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"


603 
cast_PrimT2 "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"


604 
*)


605 


606 
(* more detailed than necessary for typesafety, see above rules. *)


607 
inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *)


608 


609 
subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile> Class D\<succ>Class C"


610 
implmt: "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile> Class C\<succ>Iface I"


611 
obj_arr: "G\<turnstile>Class Object\<succ>T.[]"


612 
int_cls: "G\<turnstile> Iface I\<succ>Class C"


613 
subint: "imethds G I hidings imethds G J entails


614 
(\<lambda>(md, mh ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>


615 
\<not>G\<turnstile>I\<preceq>I J \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile> Iface I\<succ>Iface J"


616 
array: "G\<turnstile>RefT S\<succ>RefT T \<spacespace>\<Longrightarrow> G\<turnstile> RefT S.[]\<succ>RefT T.[]"


617 


618 
(*unused*)


619 
lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"


620 
apply (ind_cases "G\<turnstile>S\<succ>T")


621 
by auto


622 


623 
lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"


624 
apply (ind_cases "G\<turnstile>S\<succ>T")


625 
by auto


626 


627 
(*unused*)


628 
lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"


629 
apply (ind_cases "G\<turnstile>S\<succ>T")


630 
by auto


631 


632 
lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>


633 
\<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"


634 
apply (ind_cases "G\<turnstile>S\<succ>T")


635 
by auto


636 


637 


638 
section "casting relation"


639 


640 
inductive "cast G" intros (* casting conversion, cf. 5.5 *)


641 


642 
widen: "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"


643 
narrow: "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"


644 


645 
(*


646 
lemma ??unknown??: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>S\<succ>T\<rbrakk> \<Longrightarrow> R"


647 
deferred *)


648 


649 
(*unused*)


650 
lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"


651 
apply (ind_cases "G\<turnstile>S\<preceq>? T")


652 
by (auto dest: widen_RefT narrow_RefT)


653 


654 
lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"


655 
apply (ind_cases "G\<turnstile>S\<preceq>? T")


656 
by (auto dest: widen_RefT2 narrow_RefT2)


657 


658 
(*unused*)


659 
lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"


660 
apply (ind_cases "G\<turnstile>S\<preceq>? T")


661 
by (auto dest: widen_PrimT narrow_PrimT)


662 


663 
lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"


664 
apply (ind_cases "G\<turnstile>S\<preceq>? T")


665 
by (auto dest: widen_PrimT2 narrow_PrimT2)


666 


667 
end
