Up to index of Isabelle/Bali5
theory WellForm = WellType:(* Title: isabelle/Bali/WellForm.thy
ID: $Id: WellForm.thy,v 1.34 2001/05/11 14:42:01 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Well-formedness of Java programs
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):
* 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)
* if an interface inherits more than one method with the same signature, the
methods need not have identical return types
simplifications:
* Object and standard exceptions are assumed to be declared like normal classes
*)
theory WellForm = WellType:
section "well-formed field declarations"
(* well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3) *)
constdefs
wf_fdecl :: "prog \<Rightarrow> fdecl \<Rightarrow> bool"
"wf_fdecl G \<equiv> \<lambda>(fn,(m,ft)). is_type G ft"
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G fd = is_type G (snd (snd fd))"
apply (unfold wf_fdecl_def)
apply simp
done
section "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 *)
constdefs
wf_mhead :: "prog \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
"wf_mhead G \<equiv> \<lambda>(mn,pTs) (m,pns,rT). length pTs = length pns \<and>
( \<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT \<and>
nodups pns"
wf_mdecl :: "prog \<Rightarrow> tname \<Rightarrow> mdecl \<Rightarrow> bool"
"wf_mdecl G C \<equiv> \<lambda>((mn,pTs),(m,pns,rT),lvars,blk,res).
wf_mhead G (mn,pTs) (m,pns,rT) \<and> unique lvars \<and>
(C=Object \<longrightarrow> ¬static m) \<and> (\<forall>(vn,T)\<in>set lvars. is_type G T) \<and>
(\<forall>pn\<in>set pns. table_of lvars pn = None) \<and>
(\<exists>T. (G,table_of lvars(pns[\<mapsto>]pTs) (+)
(if static m then empty else empty(()\<mapsto>Class C)))\<turnstile>
Body C blk res\<Colon>-T \<and> G\<turnstile>T\<preceq>rT)"
lemma wf_mheadI: "\<lbrakk>length pTs = length pns;
\<forall>T\<in>set pTs. is_type G T; is_type G rT; nodups pns\<rbrakk> \<Longrightarrow>
wf_mhead G (mn, pTs) (m, pns, rT)"
apply (unfold wf_mhead_def)
apply (simp (no_asm_simp))
done
lemma wf_mdeclI: "\<lbrakk>(C = Object \<longrightarrow> ¬ static m);
wf_mhead G (mn, pTs) (m, pns, rT); unique lvars;
(\<forall>pn\<in>set pns. table_of lvars pn = None);
\<forall>(vn,T)\<in>set lvars. is_type G T;
(G, table_of lvars(pns[\<mapsto>]pTs) (+)
(if static m then empty else empty(()\<mapsto>Class C)))\<turnstile>Body C blk res\<Colon>-T;
G\<turnstile>T\<preceq>rT\<rbrakk> \<Longrightarrow>
wf_mdecl G C ((mn, pTs), (m, pns, rT), lvars, blk, res)"
apply (unfold wf_mdecl_def)
apply (auto split del: split_if split_if_asm)
done
lemma wf_mdeclD1:
"\<And>sig. wf_mdecl G C (sig,(m,pns,rT),lvars,blk,res) \<Longrightarrow>
wf_mhead G sig (m,pns,rT) \<and> unique lvars \<and>
(\<forall>pn\<in>set pns. table_of lvars pn = None) \<and> (\<forall>(vn,T)\<in>set lvars. is_type G T)"
apply (unfold wf_mdecl_def)
apply auto
done
lemma wf_mdecl_bodyD:
"\<And>sig. wf_mdecl G C (sig,(m,pns,rT),lvars,blk,res) \<Longrightarrow>
(\<exists>T. (G,table_of lvars(pns[\<mapsto>](snd sig)) (+)
(if static m then empty else empty(()\<mapsto>Class C)))\<turnstile>Body C blk res\<Colon>-T\<and> G\<turnstile>T\<preceq>rT)"
apply (unfold wf_mdecl_def)
apply auto
done
lemma static_Object_methodsE [elim!]:
"\<And>sig. wf_mdecl G Object (sig, (True, pns, T), b) \<Longrightarrow> R"
apply (unfold wf_mdecl_def)
apply auto
done
lemma rT_is_type: "\<And>sig. wf_mhead G sig (m,pns,rT) \<Longrightarrow> is_type G rT"
apply (unfold wf_mhead_def)
apply auto
done
section "well-formed interface declarations"
(* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
constdefs
wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool"
"wf_idecl G \<equiv> \<lambda>(I,(si,ms)). ws_idecl G I si \<and>
¬is_class G I \<and>
(\<forall>(sig,mh)\<in>set ms. wf_mhead G sig mh \<and> ¬static (fst mh)) \<and>
unique ms \<and>
(o2s \<circ> table_of ms hidings Un_tables((\<lambda>J.(imethds G J))`set si)
entails (\<lambda>mh (md,mh'). G\<turnstile>mrt mh\<preceq>mrt mh'))"
lemma wf_idecl_mhead: "\<And>m. \<lbrakk>wf_idecl G (I, is, ms); (s,mh)\<in>set ms\<rbrakk> \<Longrightarrow>
wf_mhead G s mh \<and> ¬static (fst mh)"
apply (unfold wf_idecl_def)
apply auto
done
lemma wf_idecl_hidings:
"wf_idecl G (I, is, ms) \<Longrightarrow> (\<lambda>s. o2s (table_of ms s)) hidings
Un_tables ((\<lambda>J. imethds G J) ` set is)
entails \<lambda>mh (md,mh'). G\<turnstile>mrt mh\<preceq>mrt mh'"
apply (unfold wf_idecl_def o_def)
apply simp
done
lemma wf_idecl_supD:
"\<lbrakk>wf_idecl G (I, is, ms); J \<in> set is\<rbrakk> \<Longrightarrow> is_iface G J \<and> (J, I) \<notin> (subint1 G)^+"
apply (unfold wf_idecl_def ws_idecl_def)
apply auto
done
section "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 *)
constdefs
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
"wf_cdecl G \<equiv> \<lambda>(C,(sc,si,fs,ms,init)).
¬is_iface G C \<and>
(\<forall>I\<in>set si. is_iface G I \<and>
(\<forall>s. \<forall>(md', mh' ) \<in> imethds G I s.
(\<exists>(md ,(mh ,b)) \<in> cmethd G C s: G\<turnstile>mrt mh\<preceq>mrt mh' \<and>
¬static (fst mh)))) \<and>
(\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and>
(\<forall>m\<in>set ms. wf_mdecl G C m) \<and> unique ms \<and>
(G,empty)\<turnstile>init\<Colon>\<surd> \<and> ws_cdecl G C sc \<and>
(C \<noteq> Object \<longrightarrow> (table_of ms hiding cmethd G sc entails
(\<lambda>(mh,b) (md',(mh',b')). G\<turnstile>mrt mh\<preceq>mrt mh' \<and>
static (fst mh') = static (fst mh))))"
lemma wf_cdecl_unique:
"wf_cdecl G (C,sc,si,fs,ms,ini) \<Longrightarrow> unique fs \<and> unique ms"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_fdecl:
"\<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); f\<in>set fs\<rbrakk> \<Longrightarrow> wf_fdecl G f"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_mdecl:
"\<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); m\<in>set ms\<rbrakk> \<Longrightarrow> wf_mdecl G C m"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_impD:
"\<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); I\<in>set si\<rbrakk> \<Longrightarrow> is_iface G I \<and>
(\<forall>s. \<forall>(md',mh') \<in> imethds G I s.
(\<exists>(md,(mh,b))\<in>cmethd G C s: G\<turnstile>mrt mh\<preceq>mrt mh' \<and> ¬static (fst mh)))"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_supD:
"\<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); C \<noteq> Object\<rbrakk> \<Longrightarrow>
is_class G sc \<and> (sc,C) \<notin> (subcls1 G)^+ \<and> (table_of ms hiding cmethd G sc
entails (\<lambda>(mh,b) (md',(mh',b')). G\<turnstile>mrt mh\<preceq>mrt mh' \<and> fst mh' = fst mh))"
apply (unfold wf_cdecl_def ws_cdecl_def)
apply auto
done
lemma wf_cdecl_wt_init:
"wf_cdecl G (C, sco, si, fs, ms, ini) \<Longrightarrow> (G, empty)\<turnstile>ini\<Colon>\<surd>"
apply (unfold wf_cdecl_def)
apply auto
done
section "well-formed programs"
(* well-formed program, cf. 8.1, 9.1 *)
constdefs
wf_prog :: "prog \<Rightarrow> bool"
"wf_prog G \<equiv> let is = fst G; cs = snd G in
ObjectC \<in> set cs \<and> (\<forall>xn. SXcptC xn \<in> set cs) \<and>
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)"
apply (unfold wf_prog_def Let_def)
apply simp
apply (fast dest: map_of_SomeD)
done
lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G"
apply (unfold wf_prog_def Let_def)
apply (rule ws_progI)
apply (simp_all (no_asm))
apply (fast dest!: wf_idecl_supD wf_cdecl_supD)+
done
lemma class_Object [simp]:
"wf_prog G \<Longrightarrow> class G Object = Some (arbitrary,[],[],Object_mdecls,Skip)"
apply (unfold wf_prog_def Let_def ObjectC_def)
apply (fast dest!: map_of_SomeI)
done
lemma class_SXcpt [simp]:
"wf_prog G \<Longrightarrow> class G (SXcpt xn) = Some (if xn = Throwable
then Object else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)"
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 \<and> Ball (set Object_mdecls)
(wf_mdecl G Object) \<and> unique Object_mdecls)"
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
apply (simp (no_asm))
done
lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object"
apply (simp (no_asm_simp))
done
lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)"
apply (simp (no_asm_simp))
done
lemma cmethd_Object: "wf_prog G \<Longrightarrow> cmethd G Object =
table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)"
apply (subst cmethd_rec)
apply auto
done
lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> fields G Object = []"
by (force intro: fields_emptyI)
lemma cfield_Object [simp]:
"wf_prog G \<Longrightarrow> cfield G Object = empty"
apply (unfold cfield_def)
apply ((simp (no_asm_simp)))
done
lemma fields_Throwable [simp]: "wf_prog G \<Longrightarrow> fields G (SXcpt Throwable) = []"
by (force intro: fields_emptyI)
lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> 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]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
apply (erule (2) widen_trans)
done
lemma Xcpt_subcls_Throwable [simp]:
"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable"
apply (rule SXcpt_subcls_Throwable_lemma)
apply auto
done
lemma unique_fields: "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (fields G C)"
apply (erule ws_unique_fields)
apply (erule wf_ws_prog)
apply safe
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
done
lemma fields_mono: "\<lbrakk>table_of (fields G C) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog G\<rbrakk>
\<Longrightarrow> table_of (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]:
"\<And>m. \<lbrakk>table_of (fields G C) m = Some(f,T); wf_prog G; is_class G C\<rbrakk> \<Longrightarrow>
is_type G T"
apply (frule wf_ws_prog)
apply (force dest: fields_defpl [THEN conjunct1]
wf_prog_cdecl [THEN wf_cdecl_fdecl]
simp add: wf_fdecl_def2)
done
lemma imethds_wf_mhead [rule_format (no_asm)]:
"\<lbrakk>(md,mh) \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow>
wf_mhead G sig mh \<and> ¬ static (fst mh)"
apply (frule wf_ws_prog)
apply (drule (2) imethds_defpl [THEN conjunct1])
apply clarify
apply (frule (1) wf_prog_idecl, erule wf_idecl_mhead, erule map_of_SomeD)
done
lemma cmethd_wf_mdecl:
"\<lbrakk>cmethd G C sig = Some (md,m); wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow>
G\<turnstile>C\<preceq>C md \<and> is_class G md \<and> wf_mdecl G md (sig,m)"
apply (frule wf_ws_prog)
apply (drule (1) cmethd_defpl)
apply fast
apply clarsimp
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
done
lemmas cmethd_rT_is_type = cmethd_wf_mdecl [THEN conjunct2, THEN conjunct2,
THEN wf_mdeclD1 [THEN conjunct1], THEN rT_is_type]
(* local lemma *)
lemma subcls_methd_: "\<And>sig. \<lbrakk>G\<turnstile>C\<preceq>C C'; is_class G C'; wf_prog G\<rbrakk> \<Longrightarrow>
\<forall>(md ,(m ,pns ,rT ),mb )\<in>cmethd G C' sig:
\<exists>(md',(m',pns',rT'),mb')\<in>cmethd G C sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT"
apply (erule converse_rtrancl_induct)
apply clarsimp
apply (drule subcls1D)
apply clarsimp
apply (subst cmethd_rec, assumption, erule wf_ws_prog)
apply (unfold override_def)
apply clarsimp
apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_supD])
apply clarsimp
apply (drule (2) hiding_entailsD)
apply clarsimp
apply fast
done
lemmas subcls_methd = subcls_methd_ [THEN ospec]
(* local lemma *)
ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *}
ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *}
lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow>
\<forall>(md, m ,pns ,rT ) \<in> imethds G J sig.
\<exists>(md',m',pns',rT') \<in> imethds G I sig. static m'=static m \<and> G\<turnstile>rT'\<preceq>rT"
apply (erule converse_rtrancl_induct)
apply (clarsimp elim!: bexI')
apply (drule subint1D)
apply clarify
apply (erule ballE')
apply fast
apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl)
apply clarsimp
apply (subst imethds_rec, assumption, erule wf_ws_prog)
apply (unfold overrides_def)
apply (drule (1) wf_prog_idecl)
apply (auto intro!: table_of_map_SomeI bexI'
dest: wf_idecl_mhead
imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1]])
apply (auto dest!: wf_idecl_hidings [THEN hidings_entailsD])
done
(* local lemma *)
lemma implmt1_methd:
"\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; (md, m, pn, rT) \<in> imethds G I sig\<rbrakk> \<Longrightarrow>
\<exists>(md',(m',pn',rT'),mb)\<in>cmethd G C sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT"
apply (drule implmt1D)
apply clarify
apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
apply (frule (1) imethds_wf_mhead)
apply simp
apply force
done
(* local lemma *)
lemma implmt_methd [rule_format (no_asm)]:
"\<lbrakk>wf_prog G; G\<turnstile>T''\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow>
(\<forall>(md, (m ,pn ,rT )) \<in>imethds G I sig.
\<exists>(md',(m',pn',rT'),mb')\<in>cmethd G T'' sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT)"
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 (drule (1) bspec)
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 subcls_methd, OF _ implmt_is_class])
apply force
done
lemma mheadsD [rule_format (no_asm)]: "(md,mh) \<in> mheads G t sig \<longrightarrow> (\<exists>C D b. t = ClassT C \<and> md = ClassT D \<and> cmethd G C sig = Some (D, mh, b)) \<or> (\<exists>I. t = IfaceT I \<and> (\<exists>I'. (I',mh) \<in> imethds G I sig) \<or> (\<exists>D b. cmethd G Object sig = Some (D, mh, b))) \<or> (\<exists>T D b. t = ArrayT T \<and> cmethd G Object sig = Some (D, mh, b))"
apply (rule ref_ty_ty.induct [THEN conjunct1])
apply (auto simp add: cmheads_def)
done
lemma class_mheadsD: "\<And>sig mh.
\<lbrakk>(md , m ,pn, rT )\<in>mheads G t sig; wf_prog G; class G C = Some y;
if (\<exists>T. t=ArrayT T) then C=Object else G\<turnstile>Class C\<preceq>RefT t; isrtype G t\<rbrakk> \<Longrightarrow>
\<exists>(md',(m',pn',rT'),mb)\<in>cmethd G C sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT"
apply (drule mheadsD)
apply safe
apply (tactic "ALLGOALS Clarsimp_tac")
apply (force dest!: subcls_methd del: bexI)
apply (drule (1) implmt_methd, simp, assumption, clarsimp)
apply (tactic {* dtac (permute_prems 0 ~1 (thm "subcls_methd")) 1 *})
apply (auto intro!: subcls_ObjectI)
done
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> E=(G,L) \<longrightarrow> wf_prog G \<longrightarrow> dt=empty_dt \<longrightarrow>
(case T of Inl T \<Rightarrow> is_type G T | Inr Ts \<Rightarrow> Ball (set Ts) (is_type G))"
apply (unfold empty_dt_def)
apply (erule wt.induct)
apply (auto split del: split_if_asm simp del: snd_conv)
apply (erule typeof_empty_is_type)
apply (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1,
force simp del: snd_conv, clarsimp)
apply (drule max_spec2mheads [THEN conjunct1, THEN mheadsD])
apply (drule_tac [2] cfield_fields)
apply (auto elim: cmethd_rT_is_type
imethds_wf_mhead [THEN conjunct1, THEN rT_is_type]
simp del: fst_conv snd_conv)
done
lemma ty_expr_is_type:
"\<lbrakk>(G, L)\<turnstile>e\<Colon>-T; wf_prog G\<rbrakk> \<Longrightarrow> is_type G T"
by (auto dest!: wt_is_type)
lemma ty_var_is_type:
"\<lbrakk>(G, L)\<turnstile>v\<Colon>=T; wf_prog G\<rbrakk> \<Longrightarrow> is_type G T"
by (auto dest!: wt_is_type)
lemma ty_exprs_is_type:
"\<lbrakk>(G, L)\<turnstile>es\<Colon>\<doteq>Ts; wf_prog G\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type G)"
by (auto dest!: wt_is_type)
lemma static_mheadsD:
"\<lbrakk>(cT, m, pns, rT) \<in> mheads G t sig; wf_prog G; (G, L)\<turnstile>e\<Colon>-RefT t;
m \<or> e = Super\<rbrakk> \<Longrightarrow> \<exists>C D b. t = ClassT C \<and> cT = ClassT D \<and>
cmethd G C sig = Some (D, (m, pns, rT), b)"
apply (frule (1) ty_expr_is_type)
apply (case_tac "m")
apply (force dest!: mheadsD imethds_wf_mhead cmethd_wf_mdecl)
apply (clarsimp, erule wt_elim_cases)
apply (auto simp add: cmheads_def)
done
lemma wt_MethdI:
"\<lbrakk>cmethd G C sig = Some (md, (m, pns, rT), lvars, blk, res); wf_prog G;
class G C = Some y\<rbrakk> \<Longrightarrow>
\<exists>T. (G, table_of lvars(pns[\<mapsto>]snd sig) (+)
(if m then empty else empty(()\<mapsto>Class md)))\<turnstile>Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>rT"
apply (frule (2) cmethd_wf_mdecl, clarify)
apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
done
end
lemma wf_fdecl_def2:
wf_fdecl G fd = is_type G (snd (snd fd))
lemma wf_mheadI:
[| length pTs = length pns; Ball (set pTs) (is_type G); is_type G rT;
nodups pns |]
==> wf_mhead G (mn, pTs) (m, pns, rT)
lemma wf_mdeclI:
[| C = Object --> ¬ id m; wf_mhead G (mn, pTs) (m, pns, rT); unique lvars;
ALL pn:set pns. table_of lvars pn = None;
Ball (set lvars) (split (%vn. is_type G));
(G, table_of lvars(pns[|->]pTs) (+)
(if id m then empty else empty(()|->Class C)))|-Body C blk res:-T;
G|-T<=:rT |]
==> wf_mdecl G C ((mn, pTs), (m, pns, rT), lvars, blk, res)
lemma wf_mdeclD1:
wf_mdecl G C (sig, (m, pns, rT), lvars, blk, res)
==> wf_mhead G sig (m, pns, rT) &
unique lvars &
(ALL pn:set pns. table_of lvars pn = None) &
Ball (set lvars) (split (%vn. is_type G))
lemma wf_mdecl_bodyD:
wf_mdecl G C (sig, (m, pns, rT), lvars, blk, res)
==> EX T. (G, table_of lvars(pns[|->]snd sig) (+)
(if id m then empty
else empty(()|->Class C)))|-Body C blk res:-T &
G|-T<=:rT
lemma static_Object_methodsE:
wf_mdecl G Object (sig, (True, pns, T), b) ==> R
lemma rT_is_type:
wf_mhead G sig (m, pns, rT) ==> is_type G rT
lemma wf_idecl_mhead:
[| wf_idecl G (I, is, ms); (s, mh) : set ms |] ==> wf_mhead G s mh & ¬ id (fst mh)
lemma wf_idecl_hidings:
wf_idecl G (I, is, ms)
==> %s. o2s (table_of ms
s) hidings Un_tables
(imethds G `
set is) entails %mh (md, mh').
G|-snd (snd mh)<=:snd (snd mh')
lemma wf_idecl_supD:
[| wf_idecl G (I, is, ms); J : set is |] ==> is_iface G J & (J, I) ~: (subint1 G)^+
lemma wf_cdecl_unique:
wf_cdecl G (C, sc, si, fs, ms, ini) ==> unique fs & unique ms
lemma wf_cdecl_fdecl:
[| wf_cdecl G (C, sc, si, fs, ms, ini); f : set fs |] ==> wf_fdecl G f
lemma wf_cdecl_mdecl:
[| wf_cdecl G (C, sc, si, fs, ms, ini); m : set ms |] ==> wf_mdecl G C m
lemma wf_cdecl_impD:
[| wf_cdecl G (C, sc, si, fs, ms, ini); I : set si |]
==> is_iface G I &
(ALL s. ALL (md', mh'):imethds G I s.
? (md, mh, b):cmethd G C s:
G|-snd (snd mh)<=:snd (snd mh') & ¬ id (fst mh))
lemma wf_cdecl_supD:
[| wf_cdecl G (C, sc, si, fs, ms, ini); C ~= Object |]
==> is_class G sc &
(sc, C) ~: (subcls1 G)^+ &
(table_of
ms hiding cmethd G
sc entails %(mh, b) (md', mh', b').
G|-snd (snd mh)<=:snd (snd mh') &
fst mh' = fst mh)
lemma wf_cdecl_wt_init:
wf_cdecl G (C, sco, si, fs, ms, ini) ==> (G, empty)|-ini:<>
lemma wf_prog_idecl:
[| iface G I = Some i; wf_prog G |] ==> wf_idecl G (I, i)
lemma wf_prog_cdecl:
[| class G C = Some c; wf_prog G |] ==> wf_cdecl G (C, c)
lemma wf_ws_prog:
wf_prog G ==> ws_prog G
lemma class_Object:
wf_prog G ==> class G Object = Some (arbitrary, [], [], Object_mdecls, Skip)
lemma class_SXcpt:
wf_prog G
==> class G (SXcpt xn) =
Some (if xn = Throwable then Object else SXcpt Throwable, [], [],
SXcpt_mdecls, Skip)
lemma wf_ObjectC:
wf_cdecl G ObjectC =
(¬ is_iface G Object &
Ball (set Object_mdecls) (wf_mdecl G Object) & unique Object_mdecls)
[!]
lemma Object_is_class:
wf_prog G ==> is_class G Object
lemma SXcpt_is_class:
wf_prog G ==> is_class G (SXcpt xn)
lemma cmethd_Object:
wf_prog G ==> cmethd G Object = table_of (map (%(s, m). (s, Object, m)) Object_mdecls)
lemma fields_Object:
wf_prog G ==> fields G Object = []
lemma cfield_Object:
wf_prog G ==> cfield G Object = empty
lemma fields_Throwable:
wf_prog G ==> fields G (SXcpt Throwable) = []
lemma fields_SXcpt:
wf_prog G ==> fields G (SXcpt xn) = []
lemmas widen_trans:
[| G|-S<=:U; G|-U<=:T; wf_prog G |] ==> G|-S<=:T [!]
lemma widen_trans2:
[| G|-U<=:T; G|-S<=:U; wf_prog G |] ==> G|-S<=:T [!]
lemma Xcpt_subcls_Throwable:
wf_prog G ==> G|-SXcpt xn<=:C SXcpt Throwable
lemma unique_fields:
[| is_class G C; wf_prog G |] ==> unique (fields G C)
lemma fields_mono:
[| table_of (fields G C) fn = Some f; G|-D<=:C C; is_class G D; wf_prog G |] ==> table_of (fields G D) fn = Some f
lemma fields_is_type:
[| table_of (fields G C) m = Some (f, T); wf_prog G; is_class G C |] ==> is_type G T
lemma imethds_wf_mhead:
[| (md, mh) : imethds G I sig; wf_prog G; is_iface G I |] ==> wf_mhead G sig mh & ¬ id (fst mh)
lemma cmethd_wf_mdecl:
[| cmethd G C sig = Some (md, m); wf_prog G; class G C = Some y |] ==> G|-C<=:C md & is_class G md & wf_mdecl G md (sig, m)
lemmas cmethd_rT_is_type:
[| cmethd G C_5 sig = Some (C_2, (m, pns, rT), lvars_2, blk_2, res_2);
wf_prog G; class G C_5 = Some y_5 |]
==> is_type G rT
lemma subcls_methd_:
[| G|-C<=:C C'; is_class G C'; wf_prog G |]
==> ! (md, (m, pns, rT), mb):cmethd G C' sig:
? (md', (m', pns', rT'), mb'):cmethd G C sig: id m' = id m & G|-rT'<=:rT
[!]
lemmas subcls_methd:
[| G_1|-C_1<=:C C'_1; is_class G_1 C'_1; wf_prog G_1;
cmethd G_1 C'_1 sig_1 = Some x |]
==> (%(md, (m, pns, rT), mb).
? (md', (m', pns', rT'), mb'):cmethd G_1 C_1 sig_1:
id m' = id m & G_1|-rT'<=:rT)
x
[term, !]
theorem bexI':
[| x : A; P x |] ==> Bex A P
theorem ballE':
[| Ball A P; x ~: A ==> Q; P x ==> Q |] ==> Q
lemma subint_widen_imethds:
[| G|-I<=:I J; wf_prog G; is_iface G J |]
==> ALL (md, m, pns, rT):imethds G J sig.
EX (md', m', pns', rT'):imethds G I sig. id m' = id m & G|-rT'<=:rT
[!]
lemma implmt1_methd:
[| G|-C~>1I; wf_prog G; (md, m, pn, rT) : imethds G I sig |] ==> ? (md', (m', pn', rT'), mb):cmethd G C sig: id m' = id m & G|-rT'<=:rT
lemma implmt_methd:
[| wf_prog G; G|-T''~>I; is_iface G I; x : imethds G I sig |]
==> (%(md, m, pn, rT).
? (md', (m', pn', rT'), mb'):cmethd G T'' sig:
id m' = id m & G|-rT'<=:rT)
x
[!]
lemma mheadsD:
(md, mh) : mheads G t sig
==> (EX C D b.
t = ClassT C & md = ClassT D & cmethd G C sig = Some (D, mh, b)) |
(EX I. t = IfaceT I & (EX I'. (I', mh) : imethds G I sig) |
(EX D b. cmethd G Object sig = Some (D, mh, b))) |
(EX T D b. t = ArrayT T & cmethd G Object sig = Some (D, mh, b))
lemma class_mheadsD:
[| (md, m, pn, rT) : mheads G t sig; wf_prog G; class G C = Some y;
if EX T. t = ArrayT T then C = Object else G|-Class C<=:RefT t;
isrtype G t |]
==> ? (md', (m', pn', rT'), mb):cmethd G C sig: id m' = id m & G|-rT'<=:rT
[!]
lemma wt_is_type:
E,dt|=v::T
==> E = (G, L) -->
wf_prog G -->
dt = empty_dt --> (is_type G (+) (%Ts. Ball (set Ts) (is_type G))) T
[!]
lemma ty_expr_is_type:
[| (G, L)|-e:-T; wf_prog G |] ==> is_type G T [!]
lemma ty_var_is_type:
[| (G, L)|-v:=T; wf_prog G |] ==> is_type G T [!]
lemma ty_exprs_is_type:
[| (G, L)|-es:#Ts; wf_prog G |] ==> Ball (set Ts) (is_type G) [!]
lemma static_mheadsD:
[| (cT, m, pns, rT) : mheads G t sig; wf_prog G; (G, L)|-e:-RefT t;
m | e = Super |]
==> EX C D b.
t = ClassT C & cT = ClassT D & cmethd G C sig = Some (D, (m, pns, rT), b)
[!]
lemma wt_MethdI:
[| cmethd G C sig = Some (md, (m, pns, rT), lvars, blk, res); wf_prog G;
class G C = Some y |]
==> EX T. (G, table_of lvars(pns[|->]snd sig) (+)
(if m then empty else empty(()|->Class md)))|-Methd C sig:-T &
G|-T<=:rT
[!]