src/HOL/Bali/WellType.thy
changeset 21765 89275a3ed7be
parent 17876 b9c92f384109
child 23747 b07cff284683
--- a/src/HOL/Bali/WellType.thy	Mon Dec 11 12:28:16 2006 +0100
+++ b/src/HOL/Bali/WellType.thy	Mon Dec 11 16:06:14 2006 +0100
@@ -245,33 +245,185 @@
 translations
   "tys"   <= (type) "ty + ty list"
 
-consts
-  wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
-(*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
-					      \<spacespace>  changing env in Try stmt *)
+
+inductive2 
+  wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
+  and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
+  and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
+  and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
+  and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
+    ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
+where
+
+  "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
+| "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
+| "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
+| "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
+
+--{* well-typed statements *}
+
+| Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
+
+| Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
+  --{* cf. 14.6 *}
+| Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
+                                         E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
+
+| Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
+	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
+
+  --{* cf. 14.8 *}
+| If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
+	  E,dt\<Turnstile>c1\<Colon>\<surd>;
+	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
+
+  --{* cf. 14.10 *}
+| Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
+	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
+  --{* cf. 14.13, 14.15, 14.16 *}
+| Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
 
-syntax
-wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
-wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
-ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
-ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
-ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
-	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
+  --{* cf. 14.16 *}
+| Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
+	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
+  --{* cf. 14.18 *}
+| Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
+	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
+          \<Longrightarrow>
+					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
+
+  --{* cf. 14.18 *}
+| Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
+
+| Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
+  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
+     The class isn't necessarily accessible from the points @{term Init} 
+     is called. Therefor we only demand @{term is_class} and not 
+     @{term is_acc_class} here. 
+   *}
+
+--{* well-typed expressions *}
+
+  --{* cf. 15.8 *}
+| NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
+  --{* cf. 15.9 *}
+| NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
+	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
+
+  --{* cf. 15.15 *}
+| Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
+	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
+
+  --{* cf. 15.19.2 *}
+| Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
+	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
+
+  --{* cf. 15.7.1 *}
+| Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Lit x\<Colon>-T"
 
-syntax (xsymbols)
-wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
-wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
-ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
-ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
-ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
-		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
+| UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
+          \<Longrightarrow>
+	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
+  
+| BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
+           T=PrimT (binop_type binop)\<rbrakk> 
+           \<Longrightarrow>
+	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
+  
+  --{* cf. 15.10.2, 15.11.1 *}
+| Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
+	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
+
+  --{* cf. 15.13.1, 15.10.1, 15.12 *}
+| Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Acc va\<Colon>-T"
+
+  --{* cf. 15.25, 15.25.1 *}
+| Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
+	  E,dt\<Turnstile>v \<Colon>-T';
+	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>va:=v\<Colon>-T'"
+
+  --{* cf. 15.24 *}
+| Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
+	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
+	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
+
+  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
+| Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
+	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
+	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
+            = {((statDeclT,m),pTs')}
+         \<rbrakk> \<Longrightarrow>
+		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
 
-translations
-	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
-	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
-	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
-	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
-	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
+| Methd: "\<lbrakk>is_class (prg E) C;
+	  methd (prg E) C sig = Some m;
+	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
+ --{* The class @{term C} is the dynamic class of the method call 
+    (cf. Eval.thy). 
+    It hasn't got to be directly accessible from the current package 
+    @{term "(pkg E)"}. 
+    Only the static class must be accessible (enshured indirectly by 
+    @{term Call}). 
+    Note that l is just a dummy value. It is only used in the smallstep 
+    semantics. To proof typesafety directly for the smallstep semantics 
+    we would have to assume conformance of l here!
+  *}
+
+| Body:	"\<lbrakk>is_class (prg E) D;
+	  E,dt\<Turnstile>blk\<Colon>\<surd>;
+	  (lcl E) Result = Some T;
+          is_type (prg E) T\<rbrakk> \<Longrightarrow>
+   					 E,dt\<Turnstile>Body D blk\<Colon>-T"
+--{* The class @{term D} implementing the method must not directly be 
+     accessible  from the current package @{term "(pkg E)"}, but can also 
+     be indirectly accessible due to inheritance (enshured in @{term Call})
+    The result type hasn't got to be accessible in Java! (If it is not 
+    accessible you can only assign it to Object).
+    For dummy value l see rule @{term Methd}. 
+   *}
+
+--{* well-typed variables *}
+
+  --{* cf. 15.13.1 *}
+| LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>LVar vn\<Colon>=T"
+  --{* cf. 15.10.1 *}
+| FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
+	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
+			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
+  --{* cf. 15.12 *}
+| AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
+	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>e.[i]\<Colon>=T"
+
+
+--{* well-typed expression lists *}
+
+  --{* cf. 15.11.??? *}
+| Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
+
+  --{* cf. 15.11.??? *}
+| Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
+	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
+					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
+
 
 syntax (* for purely static typing *)
   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
@@ -297,174 +449,6 @@
 	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
 
 
-inductive wt intros 
-
-
---{* well-typed statements *}
-
-  Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
-
-  Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
-  --{* cf. 14.6 *}
-  Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
-                                         E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
-
-  Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
-	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
-
-  --{* cf. 14.8 *}
-  If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
-	  E,dt\<Turnstile>c1\<Colon>\<surd>;
-	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
-
-  --{* cf. 14.10 *}
-  Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
-	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
-  --{* cf. 14.13, 14.15, 14.16 *}
-  Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
-
-  --{* cf. 14.16 *}
-  Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
-	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
-  --{* cf. 14.18 *}
-  Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
-	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
-          \<Longrightarrow>
-					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
-
-  --{* cf. 14.18 *}
-  Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
-
-  Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
-  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
-     The class isn't necessarily accessible from the points @{term Init} 
-     is called. Therefor we only demand @{term is_class} and not 
-     @{term is_acc_class} here. 
-   *}
-
---{* well-typed expressions *}
-
-  --{* cf. 15.8 *}
-  NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
-  --{* cf. 15.9 *}
-  NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
-	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
-
-  --{* cf. 15.15 *}
-  Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
-	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
-
-  --{* cf. 15.19.2 *}
-  Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
-	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
-
-  --{* cf. 15.7.1 *}
-  Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Lit x\<Colon>-T"
-
-  UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
-          \<Longrightarrow>
-	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
-  
-  BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
-           T=PrimT (binop_type binop)\<rbrakk> 
-           \<Longrightarrow>
-	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
-  
-  --{* cf. 15.10.2, 15.11.1 *}
-  Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
-	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
-
-  --{* cf. 15.13.1, 15.10.1, 15.12 *}
-  Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Acc va\<Colon>-T"
-
-  --{* cf. 15.25, 15.25.1 *}
-  Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
-	  E,dt\<Turnstile>v \<Colon>-T';
-	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>va:=v\<Colon>-T'"
-
-  --{* cf. 15.24 *}
-  Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
-	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
-	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
-
-  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
-  Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
-	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
-	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
-            = {((statDeclT,m),pTs')}
-         \<rbrakk> \<Longrightarrow>
-		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
-
-  Methd: "\<lbrakk>is_class (prg E) C;
-	  methd (prg E) C sig = Some m;
-	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
- --{* The class @{term C} is the dynamic class of the method call 
-    (cf. Eval.thy). 
-    It hasn't got to be directly accessible from the current package 
-    @{term "(pkg E)"}. 
-    Only the static class must be accessible (enshured indirectly by 
-    @{term Call}). 
-    Note that l is just a dummy value. It is only used in the smallstep 
-    semantics. To proof typesafety directly for the smallstep semantics 
-    we would have to assume conformance of l here!
-  *}
-
-  Body:	"\<lbrakk>is_class (prg E) D;
-	  E,dt\<Turnstile>blk\<Colon>\<surd>;
-	  (lcl E) Result = Some T;
-          is_type (prg E) T\<rbrakk> \<Longrightarrow>
-   					 E,dt\<Turnstile>Body D blk\<Colon>-T"
---{* The class @{term D} implementing the method must not directly be 
-     accessible  from the current package @{term "(pkg E)"}, but can also 
-     be indirectly accessible due to inheritance (enshured in @{term Call})
-    The result type hasn't got to be accessible in Java! (If it is not 
-    accessible you can only assign it to Object).
-    For dummy value l see rule @{term Methd}. 
-   *}
-
---{* well-typed variables *}
-
-  --{* cf. 15.13.1 *}
-  LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>LVar vn\<Colon>=T"
-  --{* cf. 15.10.1 *}
-  FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
-	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
-			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
-  --{* cf. 15.12 *}
-  AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
-	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>e.[i]\<Colon>=T"
-
-
---{* well-typed expression lists *}
-
-  --{* cf. 15.11.??? *}
-  Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
-
-  --{* cf. 15.11.??? *}
-  Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
-	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
-					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
-
-
 declare not_None_eq [simp del] 
 declare split_if [split del] split_if_asm [split del]
 declare split_paired_All [simp del] split_paired_Ex [simp del]
@@ -472,7 +456,7 @@
 change_simpset (fn ss => ss delloop "split_all_tac")
 *}
 
-inductive_cases wt_elim_cases [cases set]:
+inductive_cases2 wt_elim_cases [cases set]:
 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
@@ -610,25 +594,32 @@
     correlation. 
  *}
 
+lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
+  by (auto, frule wt_Inj_elim, auto)
+
+lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
+  by (auto, frule wt_Inj_elim, auto)
+
+lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
+  by (auto, frule wt_Inj_elim, auto)
+
+lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
+  by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
+
 ML {*
-fun wt_fun name inj rhs =
+fun wt_fun name lhs =
 let
-  val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
-  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
-	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   fun is_Inj (Const (inj,_) $ _) = true
     | is_Inj _                   = false
-  fun pred (t as (_ $ (Const ("Pair",_) $
-     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
-       x))) $ _ )) = is_Inj x
+  fun pred (_ $ _ $ _ $ _ $ x) = is_Inj x
 in
   cond_simproc name lhs pred (thm name)
 end
 
-val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
-val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
-val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
-val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
+val wt_expr_proc  = wt_fun "wt_expr_eq"  "E,dt\<Turnstile>In1l t\<Colon>U";
+val wt_var_proc   = wt_fun "wt_var_eq"   "E,dt\<Turnstile>In2 t\<Colon>U";
+val wt_exprs_proc = wt_fun "wt_exprs_eq" "E,dt\<Turnstile>In3 t\<Colon>U";
+val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "E,dt\<Turnstile>In1r t\<Colon>U";
 *}
 
 ML {*