src/HOL/Bali/WellType.thy
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13384 a34e38154413
     1.1 --- a/src/HOL/Bali/WellType.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -180,7 +180,67 @@
     1.4  apply (clarsimp simp add: invmode_IntVir_eq)
     1.5  done
     1.6  
     1.7 +consts unop_type :: "unop \<Rightarrow> prim_ty"
     1.8 +primrec 
     1.9 +"unop_type UPlus   = Integer"
    1.10 +"unop_type UMinus  = Integer"
    1.11 +"unop_type UBitNot = Integer"
    1.12 +"unop_type UNot    = Boolean"    
    1.13  
    1.14 +consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
    1.15 +primrec
    1.16 +"wt_unop UPlus   t = (t = PrimT Integer)"
    1.17 +"wt_unop UMinus  t = (t = PrimT Integer)"
    1.18 +"wt_unop UBitNot t = (t = PrimT Integer)"
    1.19 +"wt_unop UNot    t = (t = PrimT Boolean)"
    1.20 +
    1.21 +consts binop_type :: "binop \<Rightarrow> prim_ty"
    1.22 +primrec
    1.23 +"binop_type Mul      = Integer"     
    1.24 +"binop_type Div      = Integer"
    1.25 +"binop_type Mod      = Integer"
    1.26 +"binop_type Plus     = Integer"
    1.27 +"binop_type Minus    = Integer"
    1.28 +"binop_type LShift   = Integer"
    1.29 +"binop_type RShift   = Integer"
    1.30 +"binop_type RShiftU  = Integer"
    1.31 +"binop_type Less     = Boolean"
    1.32 +"binop_type Le       = Boolean"
    1.33 +"binop_type Greater  = Boolean"
    1.34 +"binop_type Ge       = Boolean"
    1.35 +"binop_type Eq       = Boolean"
    1.36 +"binop_type Neq      = Boolean"
    1.37 +"binop_type BitAnd   = Integer"
    1.38 +"binop_type And      = Boolean"
    1.39 +"binop_type BitXor   = Integer"
    1.40 +"binop_type Xor      = Boolean"
    1.41 +"binop_type BitOr    = Integer"
    1.42 +"binop_type Or       = Boolean"
    1.43 +
    1.44 +consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
    1.45 +primrec
    1.46 +"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.47 +"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.48 +"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.49 +"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.50 +"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.51 +"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.52 +"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.53 +"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.54 +"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.55 +"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.56 +"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.57 +"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.58 +"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
    1.59 +"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
    1.60 +"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.61 +"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
    1.62 +"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.63 +"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
    1.64 +"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
    1.65 +"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
    1.66 +
    1.67 +      
    1.68  types tys  =        "ty + ty list"
    1.69  translations
    1.70    "tys"   <= (type) "ty + ty list"
    1.71 @@ -237,6 +297,7 @@
    1.72  	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
    1.73  
    1.74  
    1.75 +
    1.76  inductive wt intros 
    1.77  
    1.78  
    1.79 @@ -312,6 +373,15 @@
    1.80    Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
    1.81  					 E,dt\<Turnstile>Lit x\<Colon>-T"
    1.82  
    1.83 +  UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
    1.84 +          \<Longrightarrow>
    1.85 +	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
    1.86 +  
    1.87 +  BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
    1.88 +           T=PrimT (binop_type binop)\<rbrakk> 
    1.89 +           \<Longrightarrow>
    1.90 +	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
    1.91 +  
    1.92    (* cf. 15.10.2, 15.11.1 *)
    1.93    Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
    1.94  	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
    1.95 @@ -348,6 +418,9 @@
    1.96   (* The class C is the dynamic class of the method call (cf. Eval.thy). 
    1.97    * It hasn't got to be directly accessible from the current package (pkg E). 
    1.98    * Only the static class must be accessible (enshured indirectly by Call). 
    1.99 +  * Note that l is just a dummy value. It is only used in the smallstep 
   1.100 +  * semantics. To proof typesafety directly for the smallstep semantics 
   1.101 +  * we would have to assume conformance of l here!
   1.102    *)
   1.103  
   1.104    Body:	"\<lbrakk>is_class (prg E) D;
   1.105 @@ -359,7 +432,8 @@
   1.106     * from the current package (pkg E), but can also be indirectly accessible 
   1.107     * due to inheritance (enshured in Call)
   1.108     * The result type hasn't got to be accessible in Java! (If it is not 
   1.109 -   * accessible you can only assign it to Object) 
   1.110 +   * accessible you can only assign it to Object).
   1.111 +   * For dummy value l see rule Methd. 
   1.112     *)
   1.113  
   1.114  (* well-typed variables *)
   1.115 @@ -404,6 +478,8 @@
   1.116  	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   1.117  	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   1.118  	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   1.119 +        "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   1.120 +        "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   1.121  	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   1.122  	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   1.123  	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   1.124 @@ -566,11 +642,11 @@
   1.125  apply (simp_all (no_asm_use) split del: split_if_asm)
   1.126  apply (safe del: disjE)
   1.127  (* 17 subgoals *)
   1.128 -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.129 +apply (tactic {* ALLGOALS (fn i => if i = 11 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.130  (*apply (safe del: disjE elim!: wt_elim_cases)*)
   1.131  apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   1.132  apply (simp_all (no_asm_use) split del: split_if_asm)
   1.133 -apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
   1.134 +apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   1.135  apply ((blast del: equalityCE dest: sym [THEN trans])+)
   1.136  done
   1.137