Up to index of Isabelle/Bali5
theory TypeRel = Decl(* Title: isabelle/Bali/TypeRel.thy
ID: $Id: TypeRel.thy,v 1.32 2000/11/28 23:06:20 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The relations between Java types
simplifications:
* subinterface, subclass and widening relation includes identity
improvements over Java Specification 1.0:
* 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
* one could add similar constraints also for other cases
design issues:
* the type relations do not require is_type for their arguments
* the subint1 and subcls1 relations imply is_iface/is_class for their first
arguments, which is required for their finiteness
*)
TypeRel = Decl +
consts
(*subint1, in Decl.thy*) (* direct subinterface *)
(*subint, by translation*) (* subinterface *)
(*subcls1, in Decl.thy*) (* direct subclass *)
(*subcls, by translation*) (* subclass *)
implmt1, (* direct implementation *)
implmt :: "prog \<Rightarrow> (tname × tname) set" (* implementation *)
widen, (* widening *)
narrow, (* narrowing *)
cast :: "prog \<Rightarrow> (ty × ty ) set" (* casting *)
syntax
"@subint1" :: "prog => [tname, tname] => bool" ("_|-_<:I1_" [71,71,71] 70)
"@subint" :: "prog => [tname, tname] => bool" ("_|-_<=:I _"[71,71,71] 70)
"@subcls1" :: "prog => [tname, tname] => bool" ("_|-_<:C1_" [71,71,71] 70)
"@subcls" :: "prog => [tname, tname] => bool" ("_|-_<=:C _"[71,71,71] 70)
"@implmt1" :: "prog => [tname, tname] => bool" ("_|-_~>1_" [71,71,71] 70)
"@implmt" :: "prog => [tname, tname] => 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 \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70)
"@subint" :: "prog \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70)
"@subcls1" :: "prog \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>C1_" [71,71,71] 70)
"@subcls" :: "prog \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>C _" [71,71,71] 70)
"@implmt1" :: "prog \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70)
"@implmt" :: "prog \<Rightarrow> [tname, tname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
"@widen" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
"@narrow" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
"@cast" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
translations
"G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G"
"G\<turnstile>I \<preceq>I J" == "(I,J) \<in>(subint1 G)^*" (* cf. 9.1.3 *)
"G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
"G\<turnstile>C \<preceq>C D" == "(C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
"G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G"
"G\<turnstile>C \<leadsto> I" == "(C,I) \<in> implmt G"
"G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G"
"G\<turnstile>S \<succ> T" == "(S,T) \<in> narrow G"
"G\<turnstile>S \<preceq>? T" == "(S,T) \<in> cast G"
defs
(* direct subinterface in Decl.thy, cf. 9.1.3 *)
(* direct subclass in Decl.thy, cf. 8.1.3 *)
(* direct implementation, cf. 8.1.3 *)
implmt1_def "implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (fst(snd c)))}"
inductive "implmt G" intrs (* cf. 8.1.4 *)
direct "G\<turnstile>C\<leadsto>1J \<Longrightarrow> G\<turnstile>C\<leadsto>J"
subint "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J"
subcls1 "\<lbrakk>G\<turnstile>C\<prec>C1D; G\<turnstile>D\<leadsto>J \<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J"
inductive "widen G" intrs (*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 \<Longrightarrow> 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 \<Longrightarrow> G\<turnstile> Class C\<preceq> Class D"
implmt "G\<turnstile>C\<leadsto>I \<Longrightarrow> 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 \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"
(* 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 \<Longrightarrow> \<exists>t. S=RefT t"
cast_PrimT2 "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
*)
constdefs
widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
"G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
(* more detailed than necessary for type-safety, see above rules. *)
inductive "narrow G" intrs (* narrowing reference conversion, cf. 5.1.5 *)
subcls "G\<turnstile>C\<preceq>C D \<Longrightarrow> G\<turnstile> Class D\<succ>Class C"
implmt "¬G\<turnstile>C\<leadsto>I \<Longrightarrow> 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
(\<lambda>(md, mh ) (md',mh'). G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
¬G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile> Iface I\<succ>Iface J"
array "G\<turnstile>RefT S\<succ>RefT T \<Longrightarrow> G\<turnstile> RefT S.[]\<succ>RefT T.[]"
inductive "cast G" intrs (* casting conversion, cf. 5.5 *)
widen "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
narrow "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
end
theorem implmt1D:
G|-C~>1I ==> C ~= Object & (? (sc, is, rest):class G C: I : set is)
theorem implmtD:
G|-C~>J ==> (EX I. G|-C~>1I & G|-I<=:I J) | (EX D. G|-C<:C1D & G|-D~>J)
theorem subcls_direct:
[| class G C = Some (D, rest); C ~= Object |] ==> (C, D) : (subcls1 G)^*
theorem subcls_ObjectI:
[| is_class G C; ws_prog G |] ==> G|-C<=:C Object
theorem subcls_ObjectD:
G|-Object<=:C C ==> C = Object
theorem implmt_ObjectE:
G|-Object~>I ==> R
theorem subcls_implmt:
[| G|-A<=:C B; G|-B~>K |] ==> G|-A~>K
theorem implmt_subint2:
[| G|-A~>J; G|-J<=:I K |] ==> G|-A~>K
theorem implmt_is_class:
G|-C~>I ==> is_class G C
theorem SXcpt_subcls_Throwable_lemma:
class G (SXcpt xn) = Some (if xn = Throwable then Object else SXcpt Throwable, rest) ==> G|-SXcpt xn<=:C SXcpt Throwable
theorem widen_PrimT:
G|-PrimT x<=:T ==> EX y. T = PrimT y
theorem widen_PrimT2:
G|-S<=:PrimT x ==> EX y. S = PrimT y
theorem widen_RefT:
G|-RefT R<=:T ==> EX t. T = RefT t
theorem widen_RefT2:
G|-S<=:RefT R ==> EX t. S = RefT t
theorem widen_Iface:
G|-Iface I<=:T ==> T = Class Object | (EX J. T = Iface J)
theorem widen_Iface2:
G|-S<=:Iface J ==> S = NT | (EX I. S = Iface I) | (EX D. S = Class D)
theorem widen_Iface_Iface:
G|-Iface I<=:Iface J ==> G|-I<=:I J
theorem widen_Iface_Iface_eq:
G|-Iface I<=:Iface J = G|-I<=:I J
theorem widen_Class:
G|-Class C<=:T ==> (EX D. T = Class D) | (EX I. T = Iface I)
theorem widen_Class2:
G|-S<=:Class C ==> C = Object | S = NT | (EX D. S = Class D)
theorem widen_Class_Class:
G|-Class C<=:Class cm ==> G|-C<=:C cm
theorem widen_Class_Class_eq:
G|-Class C<=:Class cm = G|-C<=:C cm
theorem widen_Class_Iface:
G|-Class C<=:Iface I ==> G|-C~>I
theorem widen_Class_Iface_eq:
G|-Class C<=:Iface I = G|-C~>I
theorem widen_Array:
G|-S.[]<=:T ==> T = Class Object | (EX T'. T = T'.[] & G|-S<=:T')
theorem widen_Array2:
G|-S<=:T.[] ==> S = NT | (EX S'. S = S'.[] & G|-S'<=:T)
theorem widen_ArrayPrimT:
G|-PrimT t.[]<=:T ==> T = Class Object | T = PrimT t.[]
theorem widen_ArrayRefT:
G|-RefT t.[]<=:T ==> T = Class Object | (EX s. T = RefT s.[] & G|-RefT t<=:RefT s)
theorem widen_ArrayRefT_ArrayRefT_eq:
G|-RefT T.[]<=:RefT T'.[] = G|-RefT T<=:RefT T'
theorem widen_Array_Array:
G|-T.[]<=:T'.[] ==> G|-T<=:T'
theorem widen_NT2:
G|-S<=:NT ==> S = NT
theorem widen_RefT_ObjectI:
[| ws_prog G; is_type G (RefT t) |] ==> G|-RefT t<=:Class Object
theorem widen_trans_lemma:
[| G|-S<=:U; ALL C. is_class G C --> G|-C<=:C Object; G|-U<=:T |] ==> G|-S<=:T
theorem ws_widen_trans:
[| G|-S<=:U; G|-U<=:T; ws_prog G |] ==> G|-S<=:T
theorem widen_antisym_lemma:
[| G|-S<=:T; ALL I J. G|-I<=:I J & G|-J<=:I I --> I = J;
ALL C D. G|-C<=:C D & G|-D<=:C C --> C = D; ALL I. G|-Object~>I --> False;
G|-T<=:S |]
==> S = T
theorem subint_antisym:
ws_prog G ==> antisym ((subint1 G)^*)
theorem subcls_antisym:
ws_prog G ==> antisym ((subcls1 G)^*)
theorem widen_antisym:
[| G|-S<=:T; G|-T<=:S; ws_prog G |] ==> S = T
theorem subcls_is_class:
[| G|-C<=:C D; is_class G D |] ==> is_class G C
theorem widen_ObjectD:
G|-Class Object<=:T ==> T = Class Object
theorem widens_Nil:
G\<turnstile>[][\<preceq>][]
theorem widens_Cons:
G\<turnstile>(S # Ss)[\<preceq>](T # Ts) = (G|-S<=:T & G\<turnstile>Ss[\<preceq>]Ts)
theorem narrow_RefT:
G|-RefT R:>T ==> EX t. T = RefT t
theorem narrow_RefT2:
G|-S:>RefT R ==> EX t. S = RefT t
theorem narrow_PrimT:
G|-PrimT pt:>T ==> EX t. T = PrimT t
theorem narrow_PrimT2:
G|-S:>PrimT pt ==> EX t. S = PrimT t & G|-PrimT t<=:PrimT pt
theorem cast_RefT:
G|-RefT R<=:? T ==> EX t. T = RefT t
theorem cast_RefT2:
G|-S<=:? RefT R ==> EX t. S = RefT t
theorem cast_PrimT:
G|-PrimT pt<=:? T ==> EX t. T = PrimT t
theorem cast_PrimT2:
G|-S<=:? PrimT pt ==> EX t. S = PrimT t & G|-PrimT t<=:PrimT pt