src/HOL/Bali/WellType.thy
changeset 21765 89275a3ed7be
parent 17876 b9c92f384109
child 23747 b07cff284683
     1.1 --- a/src/HOL/Bali/WellType.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -245,33 +245,185 @@
     1.4  translations
     1.5    "tys"   <= (type) "ty + ty list"
     1.6  
     1.7 -consts
     1.8 -  wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
     1.9 -(*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
    1.10 -					      \<spacespace>  changing env in Try stmt *)
    1.11 +
    1.12 +inductive2 
    1.13 +  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
    1.14 +  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
    1.15 +  and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
    1.16 +  and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
    1.17 +  and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
    1.18 +    ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
    1.19 +where
    1.20 +
    1.21 +  "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
    1.22 +| "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
    1.23 +| "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
    1.24 +| "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
    1.25 +
    1.26 +--{* well-typed statements *}
    1.27 +
    1.28 +| Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
    1.29 +
    1.30 +| Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
    1.31 +					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
    1.32 +  --{* cf. 14.6 *}
    1.33 +| Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
    1.34 +                                         E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
    1.35 +
    1.36 +| Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
    1.37 +	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
    1.38 +					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
    1.39 +
    1.40 +  --{* cf. 14.8 *}
    1.41 +| If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
    1.42 +	  E,dt\<Turnstile>c1\<Colon>\<surd>;
    1.43 +	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
    1.44 +					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
    1.45 +
    1.46 +  --{* cf. 14.10 *}
    1.47 +| Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
    1.48 +	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
    1.49 +					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
    1.50 +  --{* cf. 14.13, 14.15, 14.16 *}
    1.51 +| Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
    1.52  
    1.53 -syntax
    1.54 -wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
    1.55 -wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
    1.56 -ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
    1.57 -ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
    1.58 -ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
    1.59 -	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
    1.60 +  --{* cf. 14.16 *}
    1.61 +| Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
    1.62 +	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
    1.63 +					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
    1.64 +  --{* cf. 14.18 *}
    1.65 +| Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
    1.66 +	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
    1.67 +          \<Longrightarrow>
    1.68 +					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
    1.69 +
    1.70 +  --{* cf. 14.18 *}
    1.71 +| Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
    1.72 +					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
    1.73 +
    1.74 +| Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
    1.75 +					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
    1.76 +  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
    1.77 +     The class isn't necessarily accessible from the points @{term Init} 
    1.78 +     is called. Therefor we only demand @{term is_class} and not 
    1.79 +     @{term is_acc_class} here. 
    1.80 +   *}
    1.81 +
    1.82 +--{* well-typed expressions *}
    1.83 +
    1.84 +  --{* cf. 15.8 *}
    1.85 +| NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
    1.86 +					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
    1.87 +  --{* cf. 15.9 *}
    1.88 +| NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
    1.89 +	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
    1.90 +					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
    1.91 +
    1.92 +  --{* cf. 15.15 *}
    1.93 +| Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
    1.94 +	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
    1.95 +					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
    1.96 +
    1.97 +  --{* cf. 15.19.2 *}
    1.98 +| Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
    1.99 +	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   1.100 +					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   1.101 +
   1.102 +  --{* cf. 15.7.1 *}
   1.103 +| Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   1.104 +					 E,dt\<Turnstile>Lit x\<Colon>-T"
   1.105  
   1.106 -syntax (xsymbols)
   1.107 -wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   1.108 -wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   1.109 -ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   1.110 -ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   1.111 -ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   1.112 -		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   1.113 +| UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   1.114 +          \<Longrightarrow>
   1.115 +	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   1.116 +  
   1.117 +| BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   1.118 +           T=PrimT (binop_type binop)\<rbrakk> 
   1.119 +           \<Longrightarrow>
   1.120 +	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   1.121 +  
   1.122 +  --{* cf. 15.10.2, 15.11.1 *}
   1.123 +| Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   1.124 +	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   1.125 +					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   1.126 +
   1.127 +  --{* cf. 15.13.1, 15.10.1, 15.12 *}
   1.128 +| Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   1.129 +					 E,dt\<Turnstile>Acc va\<Colon>-T"
   1.130 +
   1.131 +  --{* cf. 15.25, 15.25.1 *}
   1.132 +| Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   1.133 +	  E,dt\<Turnstile>v \<Colon>-T';
   1.134 +	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   1.135 +					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   1.136 +
   1.137 +  --{* cf. 15.24 *}
   1.138 +| Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   1.139 +	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   1.140 +	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   1.141 +					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   1.142 +
   1.143 +  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   1.144 +| Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   1.145 +	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   1.146 +	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   1.147 +            = {((statDeclT,m),pTs')}
   1.148 +         \<rbrakk> \<Longrightarrow>
   1.149 +		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   1.150  
   1.151 -translations
   1.152 -	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
   1.153 -	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   1.154 -	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
   1.155 -	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
   1.156 -	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
   1.157 +| Methd: "\<lbrakk>is_class (prg E) C;
   1.158 +	  methd (prg E) C sig = Some m;
   1.159 +	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.160 +					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   1.161 + --{* The class @{term C} is the dynamic class of the method call 
   1.162 +    (cf. Eval.thy). 
   1.163 +    It hasn't got to be directly accessible from the current package 
   1.164 +    @{term "(pkg E)"}. 
   1.165 +    Only the static class must be accessible (enshured indirectly by 
   1.166 +    @{term Call}). 
   1.167 +    Note that l is just a dummy value. It is only used in the smallstep 
   1.168 +    semantics. To proof typesafety directly for the smallstep semantics 
   1.169 +    we would have to assume conformance of l here!
   1.170 +  *}
   1.171 +
   1.172 +| Body:	"\<lbrakk>is_class (prg E) D;
   1.173 +	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   1.174 +	  (lcl E) Result = Some T;
   1.175 +          is_type (prg E) T\<rbrakk> \<Longrightarrow>
   1.176 +   					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   1.177 +--{* The class @{term D} implementing the method must not directly be 
   1.178 +     accessible  from the current package @{term "(pkg E)"}, but can also 
   1.179 +     be indirectly accessible due to inheritance (enshured in @{term Call})
   1.180 +    The result type hasn't got to be accessible in Java! (If it is not 
   1.181 +    accessible you can only assign it to Object).
   1.182 +    For dummy value l see rule @{term Methd}. 
   1.183 +   *}
   1.184 +
   1.185 +--{* well-typed variables *}
   1.186 +
   1.187 +  --{* cf. 15.13.1 *}
   1.188 +| LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   1.189 +					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   1.190 +  --{* cf. 15.10.1 *}
   1.191 +| FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   1.192 +	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   1.193 +			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   1.194 +  --{* cf. 15.12 *}
   1.195 +| AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   1.196 +	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.197 +					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   1.198 +
   1.199 +
   1.200 +--{* well-typed expression lists *}
   1.201 +
   1.202 +  --{* cf. 15.11.??? *}
   1.203 +| Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   1.204 +
   1.205 +  --{* cf. 15.11.??? *}
   1.206 +| Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   1.207 +	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   1.208 +					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   1.209 +
   1.210  
   1.211  syntax (* for purely static typing *)
   1.212    wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   1.213 @@ -297,174 +449,6 @@
   1.214  	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
   1.215  
   1.216  
   1.217 -inductive wt intros 
   1.218 -
   1.219 -
   1.220 ---{* well-typed statements *}
   1.221 -
   1.222 -  Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   1.223 -
   1.224 -  Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.225 -					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   1.226 -  --{* cf. 14.6 *}
   1.227 -  Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   1.228 -                                         E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   1.229 -
   1.230 -  Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   1.231 -	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.232 -					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   1.233 -
   1.234 -  --{* cf. 14.8 *}
   1.235 -  If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.236 -	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   1.237 -	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.238 -					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   1.239 -
   1.240 -  --{* cf. 14.10 *}
   1.241 -  Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.242 -	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.243 -					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   1.244 -  --{* cf. 14.13, 14.15, 14.16 *}
   1.245 -  Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   1.246 -
   1.247 -  --{* cf. 14.16 *}
   1.248 -  Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   1.249 -	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   1.250 -					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   1.251 -  --{* cf. 14.18 *}
   1.252 -  Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   1.253 -	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   1.254 -          \<Longrightarrow>
   1.255 -					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   1.256 -
   1.257 -  --{* cf. 14.18 *}
   1.258 -  Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.259 -					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   1.260 -
   1.261 -  Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   1.262 -					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   1.263 -  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   1.264 -     The class isn't necessarily accessible from the points @{term Init} 
   1.265 -     is called. Therefor we only demand @{term is_class} and not 
   1.266 -     @{term is_acc_class} here. 
   1.267 -   *}
   1.268 -
   1.269 ---{* well-typed expressions *}
   1.270 -
   1.271 -  --{* cf. 15.8 *}
   1.272 -  NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   1.273 -					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   1.274 -  --{* cf. 15.9 *}
   1.275 -  NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   1.276 -	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.277 -					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   1.278 -
   1.279 -  --{* cf. 15.15 *}
   1.280 -  Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   1.281 -	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   1.282 -					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   1.283 -
   1.284 -  --{* cf. 15.19.2 *}
   1.285 -  Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   1.286 -	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   1.287 -					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   1.288 -
   1.289 -  --{* cf. 15.7.1 *}
   1.290 -  Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   1.291 -					 E,dt\<Turnstile>Lit x\<Colon>-T"
   1.292 -
   1.293 -  UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   1.294 -          \<Longrightarrow>
   1.295 -	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   1.296 -  
   1.297 -  BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   1.298 -           T=PrimT (binop_type binop)\<rbrakk> 
   1.299 -           \<Longrightarrow>
   1.300 -	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   1.301 -  
   1.302 -  --{* cf. 15.10.2, 15.11.1 *}
   1.303 -  Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   1.304 -	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   1.305 -					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   1.306 -
   1.307 -  --{* cf. 15.13.1, 15.10.1, 15.12 *}
   1.308 -  Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   1.309 -					 E,dt\<Turnstile>Acc va\<Colon>-T"
   1.310 -
   1.311 -  --{* cf. 15.25, 15.25.1 *}
   1.312 -  Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   1.313 -	  E,dt\<Turnstile>v \<Colon>-T';
   1.314 -	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   1.315 -					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   1.316 -
   1.317 -  --{* cf. 15.24 *}
   1.318 -  Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   1.319 -	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   1.320 -	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   1.321 -					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   1.322 -
   1.323 -  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   1.324 -  Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   1.325 -	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   1.326 -	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   1.327 -            = {((statDeclT,m),pTs')}
   1.328 -         \<rbrakk> \<Longrightarrow>
   1.329 -		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   1.330 -
   1.331 -  Methd: "\<lbrakk>is_class (prg E) C;
   1.332 -	  methd (prg E) C sig = Some m;
   1.333 -	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.334 -					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   1.335 - --{* The class @{term C} is the dynamic class of the method call 
   1.336 -    (cf. Eval.thy). 
   1.337 -    It hasn't got to be directly accessible from the current package 
   1.338 -    @{term "(pkg E)"}. 
   1.339 -    Only the static class must be accessible (enshured indirectly by 
   1.340 -    @{term Call}). 
   1.341 -    Note that l is just a dummy value. It is only used in the smallstep 
   1.342 -    semantics. To proof typesafety directly for the smallstep semantics 
   1.343 -    we would have to assume conformance of l here!
   1.344 -  *}
   1.345 -
   1.346 -  Body:	"\<lbrakk>is_class (prg E) D;
   1.347 -	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   1.348 -	  (lcl E) Result = Some T;
   1.349 -          is_type (prg E) T\<rbrakk> \<Longrightarrow>
   1.350 -   					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   1.351 ---{* The class @{term D} implementing the method must not directly be 
   1.352 -     accessible  from the current package @{term "(pkg E)"}, but can also 
   1.353 -     be indirectly accessible due to inheritance (enshured in @{term Call})
   1.354 -    The result type hasn't got to be accessible in Java! (If it is not 
   1.355 -    accessible you can only assign it to Object).
   1.356 -    For dummy value l see rule @{term Methd}. 
   1.357 -   *}
   1.358 -
   1.359 ---{* well-typed variables *}
   1.360 -
   1.361 -  --{* cf. 15.13.1 *}
   1.362 -  LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   1.363 -					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   1.364 -  --{* cf. 15.10.1 *}
   1.365 -  FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   1.366 -	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   1.367 -			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   1.368 -  --{* cf. 15.12 *}
   1.369 -  AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   1.370 -	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.371 -					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   1.372 -
   1.373 -
   1.374 ---{* well-typed expression lists *}
   1.375 -
   1.376 -  --{* cf. 15.11.??? *}
   1.377 -  Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   1.378 -
   1.379 -  --{* cf. 15.11.??? *}
   1.380 -  Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   1.381 -	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   1.382 -					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   1.383 -
   1.384 -
   1.385  declare not_None_eq [simp del] 
   1.386  declare split_if [split del] split_if_asm [split del]
   1.387  declare split_paired_All [simp del] split_paired_Ex [simp del]
   1.388 @@ -472,7 +456,7 @@
   1.389  change_simpset (fn ss => ss delloop "split_all_tac")
   1.390  *}
   1.391  
   1.392 -inductive_cases wt_elim_cases [cases set]:
   1.393 +inductive_cases2 wt_elim_cases [cases set]:
   1.394  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   1.395  	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   1.396  	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   1.397 @@ -610,25 +594,32 @@
   1.398      correlation. 
   1.399   *}
   1.400  
   1.401 +lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
   1.402 +  by (auto, frule wt_Inj_elim, auto)
   1.403 +
   1.404 +lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
   1.405 +  by (auto, frule wt_Inj_elim, auto)
   1.406 +
   1.407 +lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
   1.408 +  by (auto, frule wt_Inj_elim, auto)
   1.409 +
   1.410 +lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   1.411 +  by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
   1.412 +
   1.413  ML {*
   1.414 -fun wt_fun name inj rhs =
   1.415 +fun wt_fun name lhs =
   1.416  let
   1.417 -  val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   1.418 -  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   1.419 -	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   1.420    fun is_Inj (Const (inj,_) $ _) = true
   1.421      | is_Inj _                   = false
   1.422 -  fun pred (t as (_ $ (Const ("Pair",_) $
   1.423 -     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   1.424 -       x))) $ _ )) = is_Inj x
   1.425 +  fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
   1.426  in
   1.427    cond_simproc name lhs pred (thm name)
   1.428  end
   1.429  
   1.430 -val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   1.431 -val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   1.432 -val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   1.433 -val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   1.434 +val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
   1.435 +val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
   1.436 +val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
   1.437 +val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
   1.438  *}
   1.439  
   1.440  ML {*