1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Bali/WellType.thy Mon Jan 28 17:00:19 2002 +0100
1.3 @@ -0,0 +1,598 @@
1.4 +(* Title: isabelle/Bali/WellType.thy
1.5 + ID: $Id$
1.6 + Author: David von Oheimb
1.7 + Copyright 1997 Technische Universitaet Muenchen
1.8 +*)
1.9 +header {* Well-typedness of Java programs *}
1.10 +
1.11 +theory WellType = DeclConcepts:
1.12 +
1.13 +text {*
1.14 +improvements over Java Specification 1.0:
1.15 +\begin{itemize}
1.16 +\item methods of Object can be called upon references of interface or array type
1.17 +\end{itemize}
1.18 +simplifications:
1.19 +\begin{itemize}
1.20 +\item the type rules include all static checks on statements and expressions,
1.21 + e.g. definedness of names (of parameters, locals, fields, methods)
1.22 +\end{itemize}
1.23 +design issues:
1.24 +\begin{itemize}
1.25 +\item unified type judgment for statements, variables, expressions,
1.26 + expression lists
1.27 +\item statements are typed like expressions with dummy type Void
1.28 +\item the typing rules take an extra argument that is capable of determining
1.29 + the dynamic type of objects. Therefore, they can be used for both
1.30 + checking static types and determining runtime types in transition semantics.
1.31 +\end{itemize}
1.32 +*}
1.33 +
1.34 +types lenv
1.35 + = "(lname, ty) table" (* local variables, including This and Result *)
1.36 +
1.37 +record env =
1.38 + prg:: "prog" (* program *)
1.39 + cls:: "qtname" (* current package and class name *)
1.40 + lcl:: "lenv" (* local environment *)
1.41 +
1.42 +translations
1.43 + "lenv" <= (type) "(lname, ty) table"
1.44 + "lenv" <= (type) "lname \<Rightarrow> ty option"
1.45 + "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
1.46 + "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
1.47 +
1.48 +
1.49 +
1.50 +syntax
1.51 + pkg :: "env \<Rightarrow> pname" (* select the current package from an environment *)
1.52 +translations
1.53 + "pkg e" == "pid (cls e)"
1.54 +
1.55 +section "Static overloading: maximally specific methods "
1.56 +
1.57 +types
1.58 + emhead = "ref_ty \<times> mhead"
1.59 +
1.60 +(* Some mnemotic selectors for emhead *)
1.61 +constdefs
1.62 + "declrefT" :: "emhead \<Rightarrow> ref_ty"
1.63 + "declrefT \<equiv> fst"
1.64 +
1.65 + "mhd" :: "emhead \<Rightarrow> mhead"
1.66 + "mhd \<equiv> snd"
1.67 +
1.68 +lemma declrefT_simp[simp]:"declrefT (r,m) = r"
1.69 +by (simp add: declrefT_def)
1.70 +
1.71 +lemma mhd_simp[simp]:"mhd (r,m) = m"
1.72 +by (simp add: mhd_def)
1.73 +
1.74 +lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
1.75 +by (cases m) (simp add: member_is_static_simp mhd_def)
1.76 +
1.77 +lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
1.78 +by (cases m) simp
1.79 +
1.80 +lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
1.81 +by (cases m) simp
1.82 +
1.83 +lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
1.84 +by (cases m) simp
1.85 +
1.86 +consts
1.87 + cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
1.88 + Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
1.89 + accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
1.90 + mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
1.91 +defs
1.92 + cmheads_def:
1.93 +"cmheads G S C
1.94 + \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
1.95 + Objectmheads_def:
1.96 +"Objectmheads G S
1.97 + \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
1.98 + ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
1.99 + accObjectmheads_def:
1.100 +"accObjectmheads G S T
1.101 + \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
1.102 + then Objectmheads G S
1.103 + else \<lambda>sig. {}"
1.104 +primrec
1.105 +"mheads G S NullT = (\<lambda>sig. {})"
1.106 +"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))
1.107 + ` accimethds G (pid S) I sig \<union>
1.108 + accObjectmheads G S (IfaceT I) sig)"
1.109 +"mheads G S (ClassT C) = cmheads G S C"
1.110 +"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
1.111 +
1.112 +
1.113 +(* more detailed than necessary for type-safety, see below. *)
1.114 +constdefs
1.115 + (* applicable methods, cf. 15.11.2.1 *)
1.116 + appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
1.117 + "appl_methds G S rt \<equiv> \<lambda> sig.
1.118 + {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and>
1.119 + G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
1.120 +
1.121 + (* more specific methods, cf. 15.11.2.2 *)
1.122 + more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
1.123 + "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
1.124 +(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
1.125 +
1.126 + (* maximally specific methods, cf. 15.11.2.2 *)
1.127 + max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
1.128 +
1.129 + "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
1.130 + (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
1.131 +(*
1.132 +rules (* all properties of more_spec, appl_methods and max_spec we actually need
1.133 + these can easily be proven from the above definitions *)
1.134 +
1.135 +max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
1.136 + mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
1.137 +*)
1.138 +
1.139 +lemma max_spec2appl_meths:
1.140 + "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig"
1.141 +by (auto simp: max_spec_def)
1.142 +
1.143 +lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>
1.144 + mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
1.145 +by (auto simp: appl_methds_def)
1.146 +
1.147 +lemma max_spec2mheads:
1.148 +"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A
1.149 + \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
1.150 +apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
1.151 +done
1.152 +
1.153 +
1.154 +constdefs
1.155 + empty_dt :: "dyn_ty"
1.156 + "empty_dt \<equiv> \<lambda>a. None"
1.157 +
1.158 + invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
1.159 +"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
1.160 +
1.161 +lemma invmode_nonstatic [simp]:
1.162 + "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
1.163 +apply (unfold invmode_def)
1.164 +apply (simp (no_asm))
1.165 +done
1.166 +
1.167 +
1.168 +lemma invmode_Static_eq [simp]: "(invmode m e = Static) = static m"
1.169 +apply (unfold invmode_def)
1.170 +apply (simp (no_asm))
1.171 +done
1.172 +
1.173 +
1.174 +lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(static m) \<and> e\<noteq>Super)"
1.175 +apply (unfold invmode_def)
1.176 +apply (simp (no_asm))
1.177 +done
1.178 +
1.179 +lemma Null_staticD:
1.180 + "a'=Null \<longrightarrow> (static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
1.181 +apply (clarsimp simp add: invmode_IntVir_eq)
1.182 +done
1.183 +
1.184 +
1.185 +types tys = "ty + ty list"
1.186 +translations
1.187 + "tys" <= (type) "ty + ty list"
1.188 +
1.189 +consts
1.190 + wt :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times> term \<times> tys) set"
1.191 +(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of
1.192 + \<spacespace> changing env in Try stmt *)
1.193 +
1.194 +syntax
1.195 +wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
1.196 +wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50)
1.197 +ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
1.198 +ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
1.199 +ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
1.200 + \<spacespace> \<spacespace> ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
1.201 +
1.202 +syntax (xsymbols)
1.203 +wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
1.204 +wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
1.205 +ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
1.206 +ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
1.207 +ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
1.208 + \<spacespace> \<spacespace> ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
1.209 +
1.210 +translations
1.211 + "E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
1.212 + "E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
1.213 + "E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
1.214 + "E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T"
1.215 + "E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T"
1.216 +
1.217 +syntax (* for purely static typing *)
1.218 + wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
1.219 + wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
1.220 + ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
1.221 + ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
1.222 + ty_exprs_:: "env \<Rightarrow> [expr list,
1.223 + \<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
1.224 +
1.225 +syntax (xsymbols)
1.226 + wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
1.227 + wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
1.228 + ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
1.229 + ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
1.230 + ty_exprs_ :: "env \<Rightarrow> [expr list,
1.231 + \<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
1.232 +
1.233 +translations
1.234 + "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
1.235 + "E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
1.236 + "E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
1.237 + "E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
1.238 + "E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
1.239 +
1.240 +
1.241 +inductive wt intros
1.242 +
1.243 +
1.244 +(* well-typed statements *)
1.245 +
1.246 + Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>"
1.247 +
1.248 + Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
1.249 + E,dt\<Turnstile>Expr e\<Colon>\<surd>"
1.250 + (* cf. 14.6 *)
1.251 + Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>
1.252 + E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>"
1.253 +
1.254 + Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>;
1.255 + E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
1.256 + E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
1.257 +
1.258 + (* cf. 14.8 *)
1.259 + If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
1.260 + E,dt\<Turnstile>c1\<Colon>\<surd>;
1.261 + E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
1.262 + E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
1.263 +
1.264 + (* cf. 14.10 *)
1.265 + Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
1.266 + E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
1.267 + E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
1.268 + (* cf. 14.13, 14.15, 14.16 *)
1.269 + Do: "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
1.270 +
1.271 + (* cf. 14.16 *)
1.272 + Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
1.273 + prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
1.274 + E,dt\<Turnstile>Throw e\<Colon>\<surd>"
1.275 + (* cf. 14.18 *)
1.276 + Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
1.277 + lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
1.278 + \<Longrightarrow>
1.279 + E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
1.280 +
1.281 + (* cf. 14.18 *)
1.282 + Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
1.283 + E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
1.284 +
1.285 + Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
1.286 + E,dt\<Turnstile>Init C\<Colon>\<surd>"
1.287 + (* Init is created on the fly during evaluation (see Eval.thy). The class
1.288 + * isn't necessarily accessible from the points Init is called. Therefor
1.289 + * we only demand is_class and not is_acc_class here
1.290 + *)
1.291 +
1.292 +(* well-typed expressions *)
1.293 +
1.294 + (* cf. 15.8 *)
1.295 + NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
1.296 + E,dt\<Turnstile>NewC C\<Colon>-Class C"
1.297 + (* cf. 15.9 *)
1.298 + NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
1.299 + E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
1.300 + E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
1.301 +
1.302 + (* cf. 15.15 *)
1.303 + Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
1.304 + prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
1.305 + E,dt\<Turnstile>Cast T' e\<Colon>-T'"
1.306 +
1.307 + (* cf. 15.19.2 *)
1.308 + Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
1.309 + prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
1.310 + E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
1.311 +
1.312 + (* cf. 15.7.1 *)
1.313 + Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
1.314 + E,dt\<Turnstile>Lit x\<Colon>-T"
1.315 +
1.316 + (* cf. 15.10.2, 15.11.1 *)
1.317 + Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
1.318 + class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
1.319 + E,dt\<Turnstile>Super\<Colon>-Class (super c)"
1.320 +
1.321 + (* cf. 15.13.1, 15.10.1, 15.12 *)
1.322 + Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
1.323 + E,dt\<Turnstile>Acc va\<Colon>-T"
1.324 +
1.325 + (* cf. 15.25, 15.25.1 *)
1.326 + Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
1.327 + E,dt\<Turnstile>v \<Colon>-T';
1.328 + prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
1.329 + E,dt\<Turnstile>va:=v\<Colon>-T'"
1.330 +
1.331 + (* cf. 15.24 *)
1.332 + Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
1.333 + E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
1.334 + prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
1.335 + E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
1.336 +
1.337 + (* cf. 15.11.1, 15.11.2, 15.11.3 *)
1.338 + Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
1.339 + E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
1.340 + max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
1.341 + = {((statDeclT,m),pTs')}
1.342 + \<rbrakk> \<Longrightarrow>
1.343 + E,dt\<Turnstile>{statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
1.344 +
1.345 + Methd: "\<lbrakk>is_class (prg E) C;
1.346 + methd (prg E) C sig = Some m;
1.347 + E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
1.348 + E,dt\<Turnstile>Methd C sig\<Colon>-T"
1.349 + (* The class C is the dynamic class of the method call (cf. Eval.thy).
1.350 + * It hasn't got to be directly accessible from the current package (pkg E).
1.351 + * Only the static class must be accessible (enshured indirectly by Call).
1.352 + *)
1.353 +
1.354 + Body: "\<lbrakk>is_class (prg E) D;
1.355 + E,dt\<Turnstile>blk\<Colon>\<surd>;
1.356 + (lcl E) Result = Some T;
1.357 + is_type (prg E) T\<rbrakk> \<Longrightarrow>
1.358 + E,dt\<Turnstile>Body D blk\<Colon>-T"
1.359 + (* the class D implementing the method must not directly be accessible
1.360 + * from the current package (pkg E), but can also be indirectly accessible
1.361 + * due to inheritance (enshured in Call)
1.362 + * The result type hasn't got to be accessible in Java! (If it is not
1.363 + * accessible you can only assign it to Object)
1.364 + *)
1.365 +
1.366 +(* well-typed variables *)
1.367 +
1.368 + (* cf. 15.13.1 *)
1.369 + LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
1.370 + E,dt\<Turnstile>LVar vn\<Colon>=T"
1.371 + (* cf. 15.10.1 *)
1.372 + FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
1.373 + accfield (prg E) (cls E) C fn = Some (fd,f)\<rbrakk> \<Longrightarrow>
1.374 + E,dt\<Turnstile>{fd,static f}e..fn\<Colon>=(type f)"
1.375 + (* cf. 15.12 *)
1.376 + AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
1.377 + E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
1.378 + E,dt\<Turnstile>e.[i]\<Colon>=T"
1.379 +
1.380 +
1.381 +(* well-typed expression lists *)
1.382 +
1.383 + (* cf. 15.11.??? *)
1.384 + Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
1.385 +
1.386 + (* cf. 15.11.??? *)
1.387 + Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
1.388 + E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
1.389 + E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
1.390 +
1.391 +
1.392 +declare not_None_eq [simp del]
1.393 +declare split_if [split del] split_if_asm [split del]
1.394 +declare split_paired_All [simp del] split_paired_Ex [simp del]
1.395 +ML_setup {*
1.396 +simpset_ref() := simpset() delloop "split_all_tac"
1.397 +*}
1.398 +inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
1.399 +inductive_cases wt_elim_cases:
1.400 + "E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
1.401 + "E,dt\<Turnstile>In2 ({fd,s}e..fn) \<Colon>T"
1.402 + "E,dt\<Turnstile>In2 (e.[i]) \<Colon>T"
1.403 + "E,dt\<Turnstile>In1l (NewC C) \<Colon>T"
1.404 + "E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T"
1.405 + "E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T"
1.406 + "E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T"
1.407 + "E,dt\<Turnstile>In1l (Lit x) \<Colon>T"
1.408 + "E,dt\<Turnstile>In1l (Super) \<Colon>T"
1.409 + "E,dt\<Turnstile>In1l (Acc va) \<Colon>T"
1.410 + "E,dt\<Turnstile>In1l (Ass va v) \<Colon>T"
1.411 + "E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T"
1.412 + "E,dt\<Turnstile>In1l ({statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
1.413 + "E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T"
1.414 + "E,dt\<Turnstile>In1l (Body D blk) \<Colon>T"
1.415 + "E,dt\<Turnstile>In3 ([]) \<Colon>Ts"
1.416 + "E,dt\<Turnstile>In3 (e#es) \<Colon>Ts"
1.417 + "E,dt\<Turnstile>In1r Skip \<Colon>x"
1.418 + "E,dt\<Turnstile>In1r (Expr e) \<Colon>x"
1.419 + "E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x"
1.420 + "E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x"
1.421 + "E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x"
1.422 + "E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x"
1.423 + "E,dt\<Turnstile>In1r (Do jump) \<Colon>x"
1.424 + "E,dt\<Turnstile>In1r (Throw e) \<Colon>x"
1.425 + "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
1.426 + "E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x"
1.427 + "E,dt\<Turnstile>In1r (Init C) \<Colon>x"
1.428 +declare not_None_eq [simp]
1.429 +declare split_if [split] split_if_asm [split]
1.430 +declare split_paired_All [simp] split_paired_Ex [simp]
1.431 +ML_setup {*
1.432 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
1.433 +*}
1.434 +
1.435 +lemma is_acc_class_is_accessible:
1.436 + "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
1.437 +by (auto simp add: is_acc_class_def)
1.438 +
1.439 +lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
1.440 +by (auto simp add: is_acc_iface_def)
1.441 +
1.442 +lemma is_acc_iface_is_accessible:
1.443 + "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
1.444 +by (auto simp add: is_acc_iface_def)
1.445 +
1.446 +lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
1.447 +by (auto simp add: is_acc_type_def)
1.448 +
1.449 +lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
1.450 +by (auto simp add: is_acc_type_def)
1.451 +
1.452 +lemma wt_Methd_is_methd:
1.453 + "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
1.454 +apply (erule_tac wt_elim_cases)
1.455 +apply clarsimp
1.456 +apply (erule is_methdI, assumption)
1.457 +done
1.458 +
1.459 +(* Special versions of some typing rules, better suited to pattern match the
1.460 + * conclusion (no selectors in the conclusion\<dots>)
1.461 + *)
1.462 +
1.463 +lemma wt_Super:
1.464 +"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
1.465 + class (prg E) C = Some c;D=super c\<rbrakk>
1.466 + \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
1.467 +by (auto elim: wt.Super)
1.468 +
1.469 +lemma wt_Call:
1.470 +"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
1.471 + max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
1.472 + = {((statDeclC,m),pTs')};rT=(resTy m);
1.473 + mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
1.474 +by (auto elim: wt.Call)
1.475 +
1.476 +
1.477 +
1.478 +lemma invocationTypeExpr_noClassD:
1.479 +"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
1.480 + \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
1.481 +proof -
1.482 + assume wt: "E\<turnstile>e\<Colon>-RefT statT"
1.483 + show ?thesis
1.484 + proof (cases "e=Super")
1.485 + case True
1.486 + with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
1.487 + then show ?thesis by blast
1.488 + next
1.489 + case False then show ?thesis
1.490 + by (auto simp add: invmode_def split: split_if_asm)
1.491 + qed
1.492 +qed
1.493 +
1.494 +lemma wt_Super:
1.495 +"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk>
1.496 +\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
1.497 +by (auto elim: wt.Super)
1.498 +
1.499 +
1.500 +lemma wt_FVar:
1.501 +"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (fd,f);
1.502 + sf=static f; fT=(type f)\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{fd,sf}e..fn\<Colon>=fT"
1.503 +by (auto elim: wt.FVar)
1.504 +
1.505 +lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
1.506 +by (auto elim: wt_elim_cases intro: "wt.Init")
1.507 +
1.508 +declare wt.Skip [iff]
1.509 +
1.510 +lemma wt_StatRef:
1.511 + "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
1.512 +apply (rule wt.Cast)
1.513 +apply (rule wt.Lit)
1.514 +apply (simp (no_asm))
1.515 +apply (simp (no_asm_simp))
1.516 +apply (rule cast.widen)
1.517 +apply (simp (no_asm))
1.518 +done
1.519 +
1.520 +lemma wt_Inj_elim:
1.521 + "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of
1.522 + In1 ec \<Rightarrow> (case ec of
1.523 + Inl e \<Rightarrow> \<exists>T. U=Inl T
1.524 + | Inr s \<Rightarrow> U=Inl (PrimT Void))
1.525 + | In2 e \<Rightarrow> (\<exists>T. U=Inl T)
1.526 + | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
1.527 +apply (erule wt.induct)
1.528 +apply auto
1.529 +done
1.530 +
1.531 +ML {*
1.532 +fun wt_fun name inj rhs =
1.533 +let
1.534 + val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
1.535 + val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
1.536 + (K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
1.537 + fun is_Inj (Const (inj,_) $ _) = true
1.538 + | is_Inj _ = false
1.539 + fun pred (t as (_ $ (Const ("Pair",_) $
1.540 + _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
1.541 + x))) $ _ )) = is_Inj x
1.542 +in
1.543 + make_simproc name lhs pred (thm name)
1.544 +end
1.545 +
1.546 +val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T"
1.547 +val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T"
1.548 +val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
1.549 +val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
1.550 +*}
1.551 +
1.552 +ML {*
1.553 +Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
1.554 +*}
1.555 +
1.556 +lemma Inj_eq_lemma [simp]:
1.557 + "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
1.558 +by auto
1.559 +
1.560 +(* unused *)
1.561 +lemma single_valued_tys_lemma [rule_format (no_asm)]:
1.562 + "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow>
1.563 + G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')"
1.564 +apply (cases "E", erule wt.induct)
1.565 +apply (safe del: disjE)
1.566 +apply (simp_all (no_asm_use) split del: split_if_asm)
1.567 +apply (safe del: disjE)
1.568 +(* 17 subgoals *)
1.569 +apply (tactic {* ALLGOALS (fn i => if i = 9 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
1.570 +(*apply (safe del: disjE elim!: wt_elim_cases)*)
1.571 +apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
1.572 +apply (simp_all (no_asm_use) split del: split_if_asm)
1.573 +apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
1.574 +apply ((blast del: equalityCE dest: sym [THEN trans])+)
1.575 +done
1.576 +
1.577 +(* unused *)
1.578 +lemma single_valued_tys:
1.579 +"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
1.580 +apply (unfold single_valued_def)
1.581 +apply clarsimp
1.582 +apply (rule single_valued_tys_lemma)
1.583 +apply (auto intro!: widen_antisym)
1.584 +done
1.585 +
1.586 +lemma typeof_empty_is_type [rule_format (no_asm)]:
1.587 + "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
1.588 +apply (rule val.induct)
1.589 +apply auto
1.590 +done
1.591 +
1.592 +(* unused *)
1.593 +lemma typeof_is_type [rule_format (no_asm)]:
1.594 + "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
1.595 +apply (rule val.induct)
1.596 +prefer 5
1.597 +apply fast
1.598 +apply (simp_all (no_asm))
1.599 +done
1.600 +
1.601 +end