src/HOL/Bali/WellType.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     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