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