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 {*