author  schirmer 
Wed, 10 Jul 2002 15:07:02 +0200  
changeset 13337  f75dfc606ac7 
parent 12925  99131847fb93 
child 13384  a34e38154413 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/WellType.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Welltypedness of Java programs *} 

7 

8 
theory WellType = DeclConcepts: 

9 

10 
text {* 

11 
improvements over Java Specification 1.0: 

12 
\begin{itemize} 

13 
\item methods of Object can be called upon references of interface or array type 

14 
\end{itemize} 

15 
simplifications: 

16 
\begin{itemize} 

17 
\item the type rules include all static checks on statements and expressions, 

18 
e.g. definedness of names (of parameters, locals, fields, methods) 

19 
\end{itemize} 

20 
design issues: 

21 
\begin{itemize} 

22 
\item unified type judgment for statements, variables, expressions, 

23 
expression lists 

24 
\item statements are typed like expressions with dummy type Void 

25 
\item the typing rules take an extra argument that is capable of determining 

26 
the dynamic type of objects. Therefore, they can be used for both 

27 
checking static types and determining runtime types in transition semantics. 

28 
\end{itemize} 

29 
*} 

30 

31 
types lenv 

32 
= "(lname, ty) table" (* local variables, including This and Result *) 

33 

34 
record env = 

35 
prg:: "prog" (* program *) 

36 
cls:: "qtname" (* current package and class name *) 

37 
lcl:: "lenv" (* local environment *) 

38 

39 
translations 

40 
"lenv" <= (type) "(lname, ty) table" 

41 
"lenv" <= (type) "lname \<Rightarrow> ty option" 

42 
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>" 

43 
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>" 

44 

45 

46 

47 
syntax 

48 
pkg :: "env \<Rightarrow> pname" (* select the current package from an environment *) 

49 
translations 

50 
"pkg e" == "pid (cls e)" 

51 

52 
section "Static overloading: maximally specific methods " 

53 

54 
types 

55 
emhead = "ref_ty \<times> mhead" 

56 

57 
(* Some mnemotic selectors for emhead *) 

58 
constdefs 

59 
"declrefT" :: "emhead \<Rightarrow> ref_ty" 

60 
"declrefT \<equiv> fst" 

61 

62 
"mhd" :: "emhead \<Rightarrow> mhead" 

63 
"mhd \<equiv> snd" 

64 

65 
lemma declrefT_simp[simp]:"declrefT (r,m) = r" 

66 
by (simp add: declrefT_def) 

67 

68 
lemma mhd_simp[simp]:"mhd (r,m) = m" 

69 
by (simp add: mhd_def) 

70 

71 
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m" 

72 
by (cases m) (simp add: member_is_static_simp mhd_def) 

73 

74 
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m" 

75 
by (cases m) simp 

76 

77 
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m" 

78 
by (cases m) simp 

79 

80 
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m" 

81 
by (cases m) simp 

82 

83 
consts 

84 
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" 

85 
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" 

86 
accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 

87 
mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 

88 
defs 

89 
cmheads_def: 

90 
"cmheads G S C 

91 
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)" 

92 
Objectmheads_def: 

93 
"Objectmheads G S 

94 
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 

95 
` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)" 

96 
accObjectmheads_def: 

97 
"accObjectmheads G S T 

98 
\<equiv> if G\<turnstile>RefT T accessible_in (pid S) 

99 
then Objectmheads G S 

100 
else \<lambda>sig. {}" 

101 
primrec 

102 
"mheads G S NullT = (\<lambda>sig. {})" 

103 
"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 

104 
` accimethds G (pid S) I sig \<union> 

105 
accObjectmheads G S (IfaceT I) sig)" 

106 
"mheads G S (ClassT C) = cmheads G S C" 

107 
"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" 

108 

109 

110 
(* more detailed than necessary for typesafety, see below. *) 

111 
constdefs 

112 
(* applicable methods, cf. 15.11.2.1 *) 

113 
appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" 

114 
"appl_methds G S rt \<equiv> \<lambda> sig. 

115 
{(mh,pTs') mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 

116 
G\<turnstile>(parTs sig)[\<preceq>]pTs'}" 

117 

118 
(* more specific methods, cf. 15.11.2.2 *) 

119 
more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" 

120 
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'" 

121 
(*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'*) 

122 

123 
(* maximally specific methods, cf. 15.11.2.2 *) 

124 
max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" 

125 

126 
"max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and> 

127 
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}" 

128 
(* 

129 
rules (* all properties of more_spec, appl_methods and max_spec we actually need 

130 
these can easily be proven from the above definitions *) 

131 

132 
max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow> 

133 
mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'" 

134 
*) 

135 

136 
lemma max_spec2appl_meths: 

137 
"x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 

138 
by (auto simp: max_spec_def) 

139 

140 
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow> 

141 
mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 

142 
by (auto simp: appl_methds_def) 

143 

144 
lemma max_spec2mheads: 

145 
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 

146 
\<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 

147 
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD) 

148 
done 

149 

150 

151 
constdefs 

152 
empty_dt :: "dyn_ty" 

153 
"empty_dt \<equiv> \<lambda>a. None" 

154 

155 
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

156 
"invmode m e \<equiv> if is_static m 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

157 
then Static 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

158 
else if e=Super then SuperM else IntVir" 
12854  159 

160 
lemma invmode_nonstatic [simp]: 

161 
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" 

162 
apply (unfold invmode_def) 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

163 
apply (simp (no_asm) add: member_is_static_simp) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

164 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

165 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

166 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

167 
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

168 
apply (unfold invmode_def) 
12854  169 
apply (simp (no_asm)) 
170 
done 

171 

172 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

173 
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" 
12854  174 
apply (unfold invmode_def) 
175 
apply (simp (no_asm)) 

176 
done 

177 

178 
lemma Null_staticD: 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

179 
"a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" 
12854  180 
apply (clarsimp simp add: invmode_IntVir_eq) 
181 
done 

182 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

183 
consts unop_type :: "unop \<Rightarrow> prim_ty" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

184 
primrec 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

185 
"unop_type UPlus = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

186 
"unop_type UMinus = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

187 
"unop_type UBitNot = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

188 
"unop_type UNot = Boolean" 
12854  189 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

190 
consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

191 
primrec 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

192 
"wt_unop UPlus t = (t = PrimT Integer)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

193 
"wt_unop UMinus t = (t = PrimT Integer)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

194 
"wt_unop UBitNot t = (t = PrimT Integer)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

195 
"wt_unop UNot t = (t = PrimT Boolean)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

196 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

197 
consts binop_type :: "binop \<Rightarrow> prim_ty" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

198 
primrec 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

199 
"binop_type Mul = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

200 
"binop_type Div = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

201 
"binop_type Mod = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

202 
"binop_type Plus = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

203 
"binop_type Minus = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

204 
"binop_type LShift = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

205 
"binop_type RShift = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

206 
"binop_type RShiftU = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

207 
"binop_type Less = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

208 
"binop_type Le = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

209 
"binop_type Greater = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

210 
"binop_type Ge = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

211 
"binop_type Eq = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

212 
"binop_type Neq = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

213 
"binop_type BitAnd = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

214 
"binop_type And = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

215 
"binop_type BitXor = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

216 
"binop_type Xor = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

217 
"binop_type BitOr = Integer" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

218 
"binop_type Or = Boolean" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

219 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

220 
consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

221 
primrec 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

222 
"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

223 
"wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

224 
"wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

225 
"wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

226 
"wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

227 
"wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

228 
"wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

229 
"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

230 
"wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

231 
"wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

232 
"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

233 
"wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

234 
"wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

235 
"wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

236 
"wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

237 
"wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

238 
"wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

239 
"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

240 
"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

241 
"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

242 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

243 

12854  244 
types tys = "ty + ty list" 
245 
translations 

246 
"tys" <= (type) "ty + ty list" 

247 

248 
consts 

249 
wt :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times> term \<times> tys) set" 

250 
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 

251 
\<spacespace> changing env in Try stmt *) 

252 

253 
syntax 

254 
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_=_::_" [51,51,51,51] 50) 

255 
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_=_:<>" [51,51,51 ] 50) 

256 
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_=_:_" [51,51,51,51] 50) 

257 
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_=_:=_" [51,51,51,51] 50) 

258 
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, 

259 
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool" ("_,_=_:#_" [51,51,51,51] 50) 

260 

261 
syntax (xsymbols) 

262 
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) 

263 
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50) 

264 
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) 

265 
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) 

266 
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, 

267 
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) 

268 

269 
translations 

270 
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt" 

271 
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" 

272 
"E,dt\<Turnstile>e\<Colon>T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T" 

273 
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T" 

274 
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T" 

275 

276 
syntax (* for purely static typing *) 

277 
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("__::_" [51,51,51] 50) 

278 
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("__:<>" [51,51 ] 50) 

279 
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("__:_" [51,51,51] 50) 

280 
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("__:=_" [51,51,51] 50) 

281 
ty_exprs_:: "env \<Rightarrow> [expr list, 

282 
\<spacespace> ty list] \<Rightarrow> bool" ("__:#_" [51,51,51] 50) 

283 

284 
syntax (xsymbols) 

285 
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) 

286 
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) 

287 
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) 

288 
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) 

289 
ty_exprs_ :: "env \<Rightarrow> [expr list, 

290 
\<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) 

291 

292 
translations 

293 
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T" 

294 
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>" 

295 
"E\<turnstile>e\<Colon>T" == "E,empty_dt\<Turnstile>e\<Colon>T" 

296 
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T" 

297 
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T" 

298 

299 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

300 

12854  301 
inductive wt intros 
302 

303 

304 
(* welltyped statements *) 

305 

306 
Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" 

307 

308 
Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T\<rbrakk> \<Longrightarrow> 

309 
E,dt\<Turnstile>Expr e\<Colon>\<surd>" 

310 
(* cf. 14.6 *) 

311 
Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> 

312 
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 

313 

314 
Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 

315 
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 

316 
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" 

317 

318 
(* cf. 14.8 *) 

319 
If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>PrimT Boolean; 

320 
E,dt\<Turnstile>c1\<Colon>\<surd>; 

321 
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 

322 
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" 

323 

324 
(* cf. 14.10 *) 

325 
Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>PrimT Boolean; 

326 
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 

327 
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" 

328 
(* cf. 14.13, 14.15, 14.16 *) 

329 
Do: "E,dt\<Turnstile>Do jump\<Colon>\<surd>" 

330 

331 
(* cf. 14.16 *) 

332 
Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Class tn; 

333 
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> 

334 
E,dt\<Turnstile>Throw e\<Colon>\<surd>" 

335 
(* cf. 14.18 *) 

336 
Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; 

337 
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> 

338 
\<Longrightarrow> 

339 
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" 

340 

341 
(* cf. 14.18 *) 

342 
Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 

343 
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" 

344 

345 
Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> 

346 
E,dt\<Turnstile>Init C\<Colon>\<surd>" 

347 
(* Init is created on the fly during evaluation (see Eval.thy). The class 

348 
* isn't necessarily accessible from the points Init is called. Therefor 

349 
* we only demand is_class and not is_acc_class here 

350 
*) 

351 

352 
(* welltyped expressions *) 

353 

354 
(* cf. 15.8 *) 

355 
NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> 

356 
E,dt\<Turnstile>NewC C\<Colon>Class C" 

357 
(* cf. 15.9 *) 

358 
NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; 

359 
E,dt\<Turnstile>i\<Colon>PrimT Integer\<rbrakk> \<Longrightarrow> 

360 
E,dt\<Turnstile>New T[i]\<Colon>T.[]" 

361 

362 
(* cf. 15.15 *) 

363 
Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T; is_acc_type (prg E) (pkg E) T'; 

364 
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> 

365 
E,dt\<Turnstile>Cast T' e\<Colon>T'" 

366 

367 
(* cf. 15.19.2 *) 

368 
Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT T; is_acc_type (prg E) (pkg E) (RefT T'); 

369 
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> 

370 
E,dt\<Turnstile>e InstOf T'\<Colon>PrimT Boolean" 

371 

372 
(* cf. 15.7.1 *) 

373 
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> 

374 
E,dt\<Turnstile>Lit x\<Colon>T" 

375 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

376 
UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

377 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

378 
E,dt\<Turnstile>UnOp unop e\<Colon>T" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

379 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

380 
BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>T1; E,dt\<Turnstile>e2\<Colon>T2; wt_binop (prg E) binop T1 T2; 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

381 
T=PrimT (binop_type binop)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

382 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

383 
E,dt\<Turnstile>BinOp binop e1 e2\<Colon>T" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

384 

12854  385 
(* cf. 15.10.2, 15.11.1 *) 
386 
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; 

387 
class (prg E) C = Some c\<rbrakk> \<Longrightarrow> 

388 
E,dt\<Turnstile>Super\<Colon>Class (super c)" 

389 

390 
(* cf. 15.13.1, 15.10.1, 15.12 *) 

391 
Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> 

392 
E,dt\<Turnstile>Acc va\<Colon>T" 

393 

394 
(* cf. 15.25, 15.25.1 *) 

395 
Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; 

396 
E,dt\<Turnstile>v \<Colon>T'; 

397 
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> 

398 
E,dt\<Turnstile>va:=v\<Colon>T'" 

399 

400 
(* cf. 15.24 *) 

401 
Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>PrimT Boolean; 

402 
E,dt\<Turnstile>e1\<Colon>T1; E,dt\<Turnstile>e2\<Colon>T2; 

403 
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> 

404 
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>T" 

405 

406 
(* cf. 15.11.1, 15.11.2, 15.11.3 *) 

407 
Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT statT; 

408 
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 

409 
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 

410 
= {((statDeclT,m),pTs')} 

411 
\<rbrakk> \<Longrightarrow> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

412 
E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>(resTy m)" 
12854  413 

414 
Methd: "\<lbrakk>is_class (prg E) C; 

415 
methd (prg E) C sig = Some m; 

416 
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>T\<rbrakk> \<Longrightarrow> 

417 
E,dt\<Turnstile>Methd C sig\<Colon>T" 

418 
(* The class C is the dynamic class of the method call (cf. Eval.thy). 

419 
* It hasn't got to be directly accessible from the current package (pkg E). 

420 
* Only the static class must be accessible (enshured indirectly by Call). 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

421 
* Note that l is just a dummy value. It is only used in the smallstep 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

422 
* semantics. To proof typesafety directly for the smallstep semantics 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

423 
* we would have to assume conformance of l here! 
12854  424 
*) 
425 

426 
Body: "\<lbrakk>is_class (prg E) D; 

427 
E,dt\<Turnstile>blk\<Colon>\<surd>; 

428 
(lcl E) Result = Some T; 

429 
is_type (prg E) T\<rbrakk> \<Longrightarrow> 

430 
E,dt\<Turnstile>Body D blk\<Colon>T" 

431 
(* the class D implementing the method must not directly be accessible 

432 
* from the current package (pkg E), but can also be indirectly accessible 

433 
* due to inheritance (enshured in Call) 

434 
* The result type hasn't got to be accessible in Java! (If it is not 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

435 
* accessible you can only assign it to Object). 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

436 
* For dummy value l see rule Methd. 
12854  437 
*) 
438 

439 
(* welltyped variables *) 

440 

441 
(* cf. 15.13.1 *) 

442 
LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> 

443 
E,dt\<Turnstile>LVar vn\<Colon>=T" 

444 
(* cf. 15.10.1 *) 

445 
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Class C; 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

446 
accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

447 
E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" 
12854  448 
(* cf. 15.12 *) 
449 
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T.[]; 

450 
E,dt\<Turnstile>i\<Colon>PrimT Integer\<rbrakk> \<Longrightarrow> 

451 
E,dt\<Turnstile>e.[i]\<Colon>=T" 

452 

453 

454 
(* welltyped expression lists *) 

455 

456 
(* cf. 15.11.??? *) 

457 
Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" 

458 

459 
(* cf. 15.11.??? *) 

460 
Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>T; 

461 
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> 

462 
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" 

463 

464 

465 
declare not_None_eq [simp del] 

466 
declare split_if [split del] split_if_asm [split del] 

467 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

468 
ML_setup {* 

469 
simpset_ref() := simpset() delloop "split_all_tac" 

470 
*} 

471 
inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>" 

472 
inductive_cases wt_elim_cases: 

473 
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

474 
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" 
12854  475 
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" 
476 
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T" 

477 
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" 

478 
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" 

479 
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" 

480 
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

481 
"E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

482 
"E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T" 
12854  483 
"E,dt\<Turnstile>In1l (Super) \<Colon>T" 
484 
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T" 

485 
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" 

486 
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

487 
"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" 
12854  488 
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" 
489 
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" 

490 
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts" 

491 
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" 

492 
"E,dt\<Turnstile>In1r Skip \<Colon>x" 

493 
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x" 

494 
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" 

495 
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" 

496 
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" 

497 
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" 

498 
"E,dt\<Turnstile>In1r (Do jump) \<Colon>x" 

499 
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x" 

500 
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" 

501 
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" 

502 
"E,dt\<Turnstile>In1r (Init C) \<Colon>x" 

503 
declare not_None_eq [simp] 

504 
declare split_if [split] split_if_asm [split] 

505 
declare split_paired_All [simp] split_paired_Ex [simp] 

506 
ML_setup {* 

507 
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) 

508 
*} 

509 

510 
lemma is_acc_class_is_accessible: 

511 
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" 

512 
by (auto simp add: is_acc_class_def) 

513 

514 
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" 

515 
by (auto simp add: is_acc_iface_def) 

516 

517 
lemma is_acc_iface_is_accessible: 

518 
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" 

519 
by (auto simp add: is_acc_iface_def) 

520 

521 
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" 

522 
by (auto simp add: is_acc_type_def) 

523 

524 
lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" 

525 
by (auto simp add: is_acc_type_def) 

526 

527 
lemma wt_Methd_is_methd: 

528 
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" 

529 
apply (erule_tac wt_elim_cases) 

530 
apply clarsimp 

531 
apply (erule is_methdI, assumption) 

532 
done 

533 

534 
(* Special versions of some typing rules, better suited to pattern match the 

535 
* conclusion (no selectors in the conclusion\<dots>) 

536 
*) 

537 

538 
lemma wt_Super: 

539 
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; 

540 
class (prg E) C = Some c;D=super c\<rbrakk> 

541 
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>Class D" 

542 
by (auto elim: wt.Super) 

543 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

544 

12854  545 
lemma wt_Call: 
546 
"\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 

547 
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

548 
= {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

549 
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>rT" 
12854  550 
by (auto elim: wt.Call) 
551 

552 

553 
lemma invocationTypeExpr_noClassD: 

554 
"\<lbrakk> E\<turnstile>e\<Colon>RefT statT\<rbrakk> 

555 
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" 

556 
proof  

557 
assume wt: "E\<turnstile>e\<Colon>RefT statT" 

558 
show ?thesis 

559 
proof (cases "e=Super") 

560 
case True 

561 
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) 

562 
then show ?thesis by blast 

563 
next 

564 
case False then show ?thesis 

565 
by (auto simp add: invmode_def split: split_if_asm) 

566 
qed 

567 
qed 

568 

569 
lemma wt_Super: 

570 
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 

571 
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>Class D" 

572 
by (auto elim: wt.Super) 

573 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

574 
lemma wt_FVar: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

575 
"\<lbrakk>E,dt\<Turnstile>e\<Colon>Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

576 
sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

577 
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

578 
by (auto dest: wt.FVar) 
12854  579 

580 

581 
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" 

582 
by (auto elim: wt_elim_cases intro: "wt.Init") 

583 

584 
declare wt.Skip [iff] 

585 

586 
lemma wt_StatRef: 

587 
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>RefT rt" 

588 
apply (rule wt.Cast) 

589 
apply (rule wt.Lit) 

590 
apply (simp (no_asm)) 

591 
apply (simp (no_asm_simp)) 

592 
apply (rule cast.widen) 

593 
apply (simp (no_asm)) 

594 
done 

595 

596 
lemma wt_Inj_elim: 

597 
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 

598 
In1 ec \<Rightarrow> (case ec of 

599 
Inl e \<Rightarrow> \<exists>T. U=Inl T 

600 
 Inr s \<Rightarrow> U=Inl (PrimT Void)) 

601 
 In2 e \<Rightarrow> (\<exists>T. U=Inl T) 

602 
 In3 e \<Rightarrow> (\<exists>T. U=Inr T)" 

603 
apply (erule wt.induct) 

604 
apply auto 

605 
done 

606 

607 
ML {* 

608 
fun wt_fun name inj rhs = 

609 
let 

610 
val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U" 

611 
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 

612 
(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac]) 

613 
fun is_Inj (Const (inj,_) $ _) = true 

614 
 is_Inj _ = false 

615 
fun pred (t as (_ $ (Const ("Pair",_) $ 

616 
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ 

617 
x))) $ _ )) = is_Inj x 

618 
in 

619 
make_simproc name lhs pred (thm name) 

620 
end 

621 

622 
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>T" 

623 
val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T" 

624 
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts" 

625 
val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>" 

626 
*} 

627 

628 
ML {* 

629 
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc] 

630 
*} 

631 

632 
lemma Inj_eq_lemma [simp]: 

633 
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" 

634 
by auto 

635 

636 
(* unused *) 

637 
lemma single_valued_tys_lemma [rule_format (no_asm)]: 

638 
"\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> 

639 
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" 

640 
apply (cases "E", erule wt.induct) 

641 
apply (safe del: disjE) 

642 
apply (simp_all (no_asm_use) split del: split_if_asm) 

643 
apply (safe del: disjE) 

644 
(* 17 subgoals *) 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

645 
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) *}) 
12854  646 
(*apply (safe del: disjE elim!: wt_elim_cases)*) 
647 
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*}) 

648 
apply (simp_all (no_asm_use) split del: split_if_asm) 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

649 
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) 
12854  650 
apply ((blast del: equalityCE dest: sym [THEN trans])+) 
651 
done 

652 

653 
(* unused *) 

654 
lemma single_valued_tys: 

655 
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" 

656 
apply (unfold single_valued_def) 

657 
apply clarsimp 

658 
apply (rule single_valued_tys_lemma) 

659 
apply (auto intro!: widen_antisym) 

660 
done 

661 

662 
lemma typeof_empty_is_type [rule_format (no_asm)]: 

663 
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" 

664 
apply (rule val.induct) 

665 
apply auto 

666 
done 

667 

668 
(* unused *) 

669 
lemma typeof_is_type [rule_format (no_asm)]: 

670 
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)" 

671 
apply (rule val.induct) 

672 
prefer 5 

673 
apply fast 

674 
apply (simp_all (no_asm)) 

675 
done 

676 

677 
end 