Up to index of Isabelle/Bali5
theory TypeRel = Decl:(* Title: isabelle/Bali/TypeRel.thy
ID: $Id: TypeRel.thy,v 1.33 2001/05/11 14:41:59 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
*)
theory TypeRel = Decl:
consts
(*subint1, in Decl.thy*) (* direct subinterface *)
(*subint , by translation*) (* subinterface *)
(*subcls1, in Decl.thy*) (* direct subclass *)
(*subcls , by translation*) (* subclass *)
implmt1 :: "prog \<Rightarrow> (tname × tname) set" (* direct implementation *)
implmt :: "prog \<Rightarrow> (tname × tname) set" (* implementation *)
widen :: "prog \<Rightarrow> (ty × ty ) set" (* widening *)
narrow :: "prog \<Rightarrow> (ty × ty ) set" (* 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"
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 SXcpt_subcls_Throwable_lemma: "\<lbrakk>class G (SXcpt xn) = Some (if xn = Throwable then Object else
SXcpt Throwable, rest)\<rbrakk> \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable"
apply (case_tac "xn = Throwable")
apply simp_all
apply (erule subcls_direct)
apply (simp (no_asm))
done
lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> 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 subcls_ObjectD [dest!]: "G\<turnstile>Object\<preceq>C C \<Longrightarrow> C = Object"
apply (erule rtrancl_induct)
apply (auto dest: subcls1D)
done
(* unused *)
lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> 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 \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
apply (erule rtrancl_induct)
apply (drule_tac [2] subcls1D)
apply auto
done
section "implementation relation"
defs
(* 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)))}"
lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>(sc,is,rest)\<in>class G C: I\<in>set is)"
apply (unfold implmt1_def)
apply auto
done
inductive "implmt G" intros (* 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"
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>C1D \<and> G\<turnstile>D\<leadsto>J)"
apply (erule implmt.induct)
apply fast+
done
lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"
by (auto dest!: implmtD implmt1D subcls1D)
lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K"
apply (erule rtrancl_induct)
apply (auto intro: implmt.subcls1)
done
lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<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.[]"
declare widen.refl [intro!]
declare widen.intros [simp]
(* too strong in general:
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
*)
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>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 \<Longrightarrow> S = PrimT x"
*)
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>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 \<Longrightarrow> 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 \<Longrightarrow> (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_ArrayRefT:
"G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> 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'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"
apply (drule widen_Array)
apply auto
done
(*
qed_typerel "widen_NT2" "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
[prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = NT \<longrightarrow> S = NT"]
*)
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
apply (ind_cases "G\<turnstile>S\<preceq>T")
by auto
lemma widen_trans_lemma [rule_format (no_asm)]:
"\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> 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: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
by (auto intro: widen_trans_lemma subcls_ObjectI)
lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;
\<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;
\<forall>C D. G\<turnstile>C\<preceq>C D \<and> G\<turnstile>D\<preceq>C C \<longrightarrow> C = D;
\<forall>I . G\<turnstile>Object\<leadsto>I \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> 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: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> T=Class Object"
apply (frule widen_Class)
apply (fast dest: widen_Class_Class widen_Class_Iface)
done
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'"
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 \<and> 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 \<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"
*)
(* 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 \<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.[]"
(*unused*)
lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
apply (ind_cases "G\<turnstile>S\<succ>T")
by auto
lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
apply (ind_cases "G\<turnstile>S\<succ>T")
by auto
(*unused*)
lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
apply (ind_cases "G\<turnstile>S\<succ>T")
by auto
lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>
\<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
apply (ind_cases "G\<turnstile>S\<succ>T")
by auto
section "casting relation"
inductive "cast G" intros (* 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"
(*
lemma ??unknown??: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>S\<succ>T\<rbrakk> \<Longrightarrow> R"
deferred *)
(*unused*)
lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>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 \<Longrightarrow> \<exists>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 \<Longrightarrow> \<exists>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 \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
apply (ind_cases "G\<turnstile>S\<preceq>? T")
by (auto dest: widen_PrimT2 narrow_PrimT2)
end
lemmas subcls_direct:
[| class G C = Some (D, rest); C ~= Object |] ==> G|-C<=:C D
lemma SXcpt_subcls_Throwable_lemma:
class G (SXcpt xn) = Some (if xn = Throwable then Object else SXcpt Throwable, rest) ==> G|-SXcpt xn<=:C SXcpt Throwable
lemma subcls_ObjectI:
[| is_class G C; ws_prog G |] ==> G|-C<=:C Object
lemma subcls_ObjectD:
G|-Object<=:C C ==> C = Object
lemma subcls_is_class:
(C, D) : (subcls1 G)^+ ==> is_class G C
lemma subcls_is_class2:
[| G|-C<=:C D; is_class G D |] ==> is_class G C
lemma implmt1D:
G|-C~>1I ==> C ~= Object & (? (sc, is, rest):class G C: I : set is)
lemma implmtD:
G|-C~>J ==> (EX I. G|-C~>1I & G|-I<=:I J) | (EX 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 ==> EX y. T = PrimT y [!]
lemma widen_PrimT2:
G|-S<=:PrimT x ==> EX y. S = PrimT y [!]
lemma widen_RefT:
G|-RefT R<=:T ==> EX t. T = RefT t [!]
lemma widen_RefT2:
G|-S<=:RefT R ==> EX t. S = RefT t [!]
lemma widen_Iface:
G|-Iface I<=:T ==> T = Class Object | (EX J. T = Iface J) [!]
lemma widen_Iface2:
G|-S<=:Iface J ==> S = NT | (EX I. S = Iface I) | (EX 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 ==> (EX D. T = Class D) | (EX I. T = Iface I) [!]
lemma widen_Class2:
G|-S<=:Class C ==> C = Object | S = NT | (EX 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 | (EX T'. T = T'.[] & G|-S<=:T') [!]
lemma widen_Array2:
G|-S<=:T.[] ==> S = NT | (EX 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 | (EX 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_NT2:
G|-S<=:NT ==> S = NT [!]
lemma widen_trans_lemma:
[| G|-S<=:U; ALL 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; 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
[!]
lemmas subint_antisym:
ws_prog G ==> antisym ((subint1 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 ==> EX t. T = RefT t [!]
lemma narrow_RefT2:
G|-S:>RefT R ==> EX t. S = RefT t [!]
lemma narrow_PrimT:
G|-PrimT pt:>T ==> EX t. T = PrimT t [!]
lemma narrow_PrimT2:
G|-S:>PrimT pt ==> EX t. S = PrimT t & G|-PrimT t<=:PrimT pt [!]
lemma cast_RefT:
G|-RefT R<=:? T ==> EX t. T = RefT t [!]
lemma cast_RefT2:
G|-S<=:? RefT R ==> EX t. S = RefT t [!]
lemma cast_PrimT:
G|-PrimT pt<=:? T ==> EX t. T = PrimT t [!]
lemma cast_PrimT2:
G|-S<=:? PrimT pt ==> EX t. S = PrimT t & G|-PrimT t<=:PrimT pt [!]