src/HOL/Bali/WellType.thy
changeset 13688 a0b16d42d489
parent 13524 604d0f3622d6
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Bali/WellType.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -29,12 +29,12 @@
     1.4  *}
     1.5  
     1.6  types	lenv
     1.7 -	= "(lname, ty) table"   (* local variables, including This and Result *)
     1.8 +	= "(lname, ty) table"  --{* local variables, including This and Result*}
     1.9  
    1.10  record env = 
    1.11 -         prg:: "prog"    (* program *)
    1.12 -         cls:: "qtname"  (* current package and class name *)
    1.13 -         lcl:: "lenv"    (* local environment *)     
    1.14 +         prg:: "prog"    --{* program *}
    1.15 +         cls:: "qtname"  --{* current package and class name *}
    1.16 +         lcl:: "lenv"    --{* local environment *}     
    1.17    
    1.18  translations
    1.19    "lenv" <= (type) "(lname, ty) table"
    1.20 @@ -45,8 +45,8 @@
    1.21  
    1.22  
    1.23  syntax
    1.24 -  pkg :: "env \<Rightarrow> pname" (* select the current package from an environment *)
    1.25 -translations
    1.26 +  pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    1.27 +translations 
    1.28    "pkg e" == "pid (cls e)"
    1.29  
    1.30  section "Static overloading: maximally specific methods "
    1.31 @@ -54,7 +54,7 @@
    1.32  types
    1.33    emhead = "ref_ty \<times> mhead"
    1.34  
    1.35 -(* Some mnemotic selectors for emhead *)
    1.36 +--{* Some mnemotic selectors for emhead *}
    1.37  constdefs 
    1.38    "declrefT" :: "emhead \<Rightarrow> ref_ty"
    1.39    "declrefT \<equiv> fst"
    1.40 @@ -106,32 +106,24 @@
    1.41  "mheads G S (ClassT C) = cmheads G S C"
    1.42  "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
    1.43  
    1.44 -
    1.45 -(* more detailed than necessary for type-safety, see below. *)
    1.46  constdefs
    1.47 -  (* applicable methods, cf. 15.11.2.1 *)
    1.48 +  --{* applicable methods, cf. 15.11.2.1 *}
    1.49    appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
    1.50   "appl_methds G S rt \<equiv> \<lambda> sig. 
    1.51        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
    1.52                             G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
    1.53  
    1.54 -  (* more specific methods, cf. 15.11.2.2 *)
    1.55 +  --{* more specific methods, cf. 15.11.2.2 *}
    1.56    more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
    1.57   "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
    1.58  (*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.59  
    1.60 -  (* maximally specific methods, cf. 15.11.2.2 *)
    1.61 +  --{* maximally specific methods, cf. 15.11.2.2 *}
    1.62     max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
    1.63  
    1.64   "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
    1.65  		      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
    1.66 -(*
    1.67 -rules (* all properties of more_spec, appl_methods and max_spec we actually need
    1.68 -         these can easily be proven from the above definitions *)
    1.69  
    1.70 -max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
    1.71 -      mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
    1.72 -*)
    1.73  
    1.74  lemma max_spec2appl_meths: 
    1.75    "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
    1.76 @@ -180,6 +172,8 @@
    1.77  apply (clarsimp simp add: invmode_IntVir_eq)
    1.78  done
    1.79  
    1.80 +section "Typing for unary operations"
    1.81 +
    1.82  consts unop_type :: "unop \<Rightarrow> prim_ty"
    1.83  primrec 
    1.84  "unop_type UPlus   = Integer"
    1.85 @@ -194,6 +188,8 @@
    1.86  "wt_unop UBitNot t = (t = PrimT Integer)"
    1.87  "wt_unop UNot    t = (t = PrimT Boolean)"
    1.88  
    1.89 +section "Typing for binary operations"
    1.90 +
    1.91  consts binop_type :: "binop \<Rightarrow> prim_ty"
    1.92  primrec
    1.93  "binop_type Mul      = Integer"     
    1.94 @@ -244,6 +240,7 @@
    1.95  "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
    1.96  "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
    1.97  
    1.98 +section "Typing for terms"
    1.99  
   1.100  types tys  =        "ty + ty list"
   1.101  translations
   1.102 @@ -295,23 +292,22 @@
   1.103  
   1.104  translations
   1.105  	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   1.106 -	"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
   1.107 -	"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
   1.108 -	"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
   1.109 -	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
   1.110 -
   1.111 +        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
   1.112 +	"E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
   1.113 +	"E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
   1.114 +	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
   1.115  
   1.116  
   1.117  inductive wt intros 
   1.118  
   1.119  
   1.120 -(* well-typed statements *)
   1.121 +--{* well-typed statements *}
   1.122  
   1.123    Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   1.124  
   1.125    Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.126  					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   1.127 -  (* cf. 14.6 *)
   1.128 +  --{* cf. 14.6 *}
   1.129    Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   1.130                                           E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   1.131  
   1.132 @@ -319,61 +315,62 @@
   1.133  	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.134  					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   1.135  
   1.136 -  (* cf. 14.8 *)
   1.137 +  --{* cf. 14.8 *}
   1.138    If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.139  	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   1.140  	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.141  					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   1.142  
   1.143 -  (* cf. 14.10 *)
   1.144 +  --{* cf. 14.10 *}
   1.145    Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.146  	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.147  					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   1.148 -  (* cf. 14.13, 14.15, 14.16 *)
   1.149 -  Do:                                   "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
   1.150 +  --{* cf. 14.13, 14.15, 14.16 *}
   1.151 +  Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   1.152  
   1.153 -  (* cf. 14.16 *)
   1.154 +  --{* cf. 14.16 *}
   1.155    Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   1.156  	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   1.157  					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   1.158 -  (* cf. 14.18 *)
   1.159 +  --{* cf. 14.18 *}
   1.160    Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   1.161  	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   1.162            \<Longrightarrow>
   1.163  					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   1.164  
   1.165 -  (* cf. 14.18 *)
   1.166 +  --{* cf. 14.18 *}
   1.167    Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.168  					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   1.169  
   1.170    Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   1.171  					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   1.172 -  (* Init is created on the fly during evaluation (see Eval.thy). The class
   1.173 -   * isn't necessarily accessible from the points Init is called. Therefor
   1.174 -   * we only demand is_class and not is_acc_class here 
   1.175 -   *)
   1.176 +  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   1.177 +     The class isn't necessarily accessible from the points @{term Init} 
   1.178 +     is called. Therefor we only demand @{term is_class} and not 
   1.179 +     @{term is_acc_class} here. 
   1.180 +   *}
   1.181  
   1.182 -(* well-typed expressions *)
   1.183 +--{* well-typed expressions *}
   1.184  
   1.185 -  (* cf. 15.8 *)
   1.186 +  --{* cf. 15.8 *}
   1.187    NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   1.188  					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   1.189 -  (* cf. 15.9 *)
   1.190 +  --{* cf. 15.9 *}
   1.191    NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   1.192  	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.193  					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   1.194  
   1.195 -  (* cf. 15.15 *)
   1.196 +  --{* cf. 15.15 *}
   1.197    Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   1.198  	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   1.199  					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   1.200  
   1.201 -  (* cf. 15.19.2 *)
   1.202 +  --{* cf. 15.19.2 *}
   1.203    Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   1.204  	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   1.205  					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   1.206  
   1.207 -  (* cf. 15.7.1 *)
   1.208 +  --{* cf. 15.7.1 *}
   1.209    Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   1.210  					 E,dt\<Turnstile>Lit x\<Colon>-T"
   1.211  
   1.212 @@ -386,28 +383,28 @@
   1.213             \<Longrightarrow>
   1.214  	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   1.215    
   1.216 -  (* cf. 15.10.2, 15.11.1 *)
   1.217 +  --{* cf. 15.10.2, 15.11.1 *}
   1.218    Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   1.219  	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   1.220  					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   1.221  
   1.222 -  (* cf. 15.13.1, 15.10.1, 15.12 *)
   1.223 +  --{* cf. 15.13.1, 15.10.1, 15.12 *}
   1.224    Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   1.225  					 E,dt\<Turnstile>Acc va\<Colon>-T"
   1.226  
   1.227 -  (* cf. 15.25, 15.25.1 *)
   1.228 +  --{* cf. 15.25, 15.25.1 *}
   1.229    Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   1.230  	  E,dt\<Turnstile>v \<Colon>-T';
   1.231  	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   1.232  					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   1.233  
   1.234 -  (* cf. 15.24 *)
   1.235 +  --{* cf. 15.24 *}
   1.236    Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   1.237  	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   1.238  	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   1.239  					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   1.240  
   1.241 -  (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   1.242 +  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   1.243    Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   1.244  	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   1.245  	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   1.246 @@ -419,48 +416,51 @@
   1.247  	  methd (prg E) C sig = Some m;
   1.248  	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.249  					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   1.250 - (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   1.251 -  * It hasn't got to be directly accessible from the current package (pkg E). 
   1.252 -  * Only the static class must be accessible (enshured indirectly by Call). 
   1.253 -  * Note that l is just a dummy value. It is only used in the smallstep 
   1.254 -  * semantics. To proof typesafety directly for the smallstep semantics 
   1.255 -  * we would have to assume conformance of l here!
   1.256 -  *)
   1.257 + --{* The class @{term C} is the dynamic class of the method call 
   1.258 +    (cf. Eval.thy). 
   1.259 +    It hasn't got to be directly accessible from the current package 
   1.260 +    @{term "(pkg E)"}. 
   1.261 +    Only the static class must be accessible (enshured indirectly by 
   1.262 +    @{term Call}). 
   1.263 +    Note that l is just a dummy value. It is only used in the smallstep 
   1.264 +    semantics. To proof typesafety directly for the smallstep semantics 
   1.265 +    we would have to assume conformance of l here!
   1.266 +  *}
   1.267  
   1.268    Body:	"\<lbrakk>is_class (prg E) D;
   1.269  	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   1.270  	  (lcl E) Result = Some T;
   1.271            is_type (prg E) T\<rbrakk> \<Longrightarrow>
   1.272     					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   1.273 -  (* the class D implementing the method must not directly be accessible 
   1.274 -   * from the current package (pkg E), but can also be indirectly accessible 
   1.275 -   * due to inheritance (enshured in Call)
   1.276 -   * The result type hasn't got to be accessible in Java! (If it is not 
   1.277 -   * accessible you can only assign it to Object).
   1.278 -   * For dummy value l see rule Methd. 
   1.279 -   *)
   1.280 +--{* The class @{term D} implementing the method must not directly be 
   1.281 +     accessible  from the current package @{term "(pkg E)"}, but can also 
   1.282 +     be indirectly accessible due to inheritance (enshured in @{term Call})
   1.283 +    The result type hasn't got to be accessible in Java! (If it is not 
   1.284 +    accessible you can only assign it to Object).
   1.285 +    For dummy value l see rule @{term Methd}. 
   1.286 +   *}
   1.287  
   1.288 -(* well-typed variables *)
   1.289 +--{* well-typed variables *}
   1.290  
   1.291 -  (* cf. 15.13.1 *)
   1.292 +  --{* cf. 15.13.1 *}
   1.293    LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   1.294  					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   1.295 -  (* cf. 15.10.1 *)
   1.296 +  --{* cf. 15.10.1 *}
   1.297    FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   1.298  	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   1.299  			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   1.300 -  (* cf. 15.12 *)
   1.301 +  --{* cf. 15.12 *}
   1.302    AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   1.303  	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.304  					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   1.305  
   1.306  
   1.307 -(* well-typed expression lists *)
   1.308 +--{* well-typed expression lists *}
   1.309  
   1.310 -  (* cf. 15.11.??? *)
   1.311 +  --{* cf. 15.11.??? *}
   1.312    Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   1.313  
   1.314 -  (* cf. 15.11.??? *)
   1.315 +  --{* cf. 15.11.??? *}
   1.316    Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   1.317  	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   1.318  					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   1.319 @@ -472,8 +472,8 @@
   1.320  ML_setup {*
   1.321  simpset_ref() := simpset() delloop "split_all_tac"
   1.322  *}
   1.323 -inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
   1.324 -inductive_cases wt_elim_cases:
   1.325 +
   1.326 +inductive_cases wt_elim_cases [cases set]:
   1.327  	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   1.328  	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   1.329  	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   1.330 @@ -499,7 +499,7 @@
   1.331          "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   1.332  	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   1.333  	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   1.334 -        "E,dt\<Turnstile>In1r (Do jump)               \<Colon>x"
   1.335 +        "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
   1.336  	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   1.337  	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   1.338  	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   1.339 @@ -536,9 +536,10 @@
   1.340  apply (erule is_methdI, assumption)
   1.341  done
   1.342  
   1.343 -(* Special versions of some typing rules, better suited to pattern match the
   1.344 - * conclusion (no selectors in the conclusion\<dots>)
   1.345 - *)
   1.346 +
   1.347 +text {* Special versions of some typing rules, better suited to pattern 
   1.348 +        match the conclusion (no selectors in the conclusion)
   1.349 +*}
   1.350  
   1.351  lemma wt_Call: 
   1.352  "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   1.353 @@ -602,6 +603,14 @@
   1.354  apply auto
   1.355  done
   1.356  
   1.357 +--{* In the special syntax to distinguish the typing judgements for expressions, 
   1.358 +     statements, variables and expression lists the kind of term corresponds
   1.359 +     to the kind of type in the end e.g. An statement (injection @{term In3} 
   1.360 +    into terms, always has type void (injection @{term Inl} into the generalised
   1.361 +    types. The following simplification procedures establish these kinds of
   1.362 +    correlation. 
   1.363 + *}
   1.364 +
   1.365  ML {*
   1.366  fun wt_fun name inj rhs =
   1.367  let
   1.368 @@ -627,6 +636,19 @@
   1.369  Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   1.370  *}
   1.371  
   1.372 +lemma wt_elim_BinOp:
   1.373 +  "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   1.374 +    \<And>T1 T2 T3.
   1.375 +       \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   1.376 +          E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   1.377 +          T = Inl (PrimT (binop_type binop))\<rbrakk>
   1.378 +       \<Longrightarrow> P\<rbrakk>
   1.379 +\<Longrightarrow> P"
   1.380 +apply (erule wt_elim_cases)
   1.381 +apply (cases b)
   1.382 +apply auto
   1.383 +done
   1.384 +
   1.385  lemma Inj_eq_lemma [simp]: 
   1.386    "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   1.387  by auto