author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14981  e73f8140af78 
child 18447  da548623916a 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/TypeRel.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

5 
header {* The relations between Java types *} 

6 

16417  7 
theory TypeRel imports Decl begin 
12854  8 

9 
text {* 

10 
simplifications: 

11 
\begin{itemize} 

12 
\item subinterface, subclass and widening relation includes identity 

13 
\end{itemize} 

14 
improvements over Java Specification 1.0: 

15 
\begin{itemize} 

16 
\item narrowing reference conversion also in cases where the return types of a 

17 
pair of methods common to both types are in widening (rather identity) 

18 
relation 

19 
\item one could add similar constraints also for other cases 

20 
\end{itemize} 

21 
design issues: 

22 
\begin{itemize} 

23 
\item the type relations do not require @{text is_type} for their arguments 

24 
\item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class} 

25 
for their first arguments, which is required for their finiteness 

26 
\end{itemize} 

27 
*} 

28 

29 
consts 

30 

14674  31 
(*subint1, in Decl.thy*) (* direct subinterface *) 
32 
(*subint , by translation*) (* subinterface (+ identity) *) 

33 
(*subcls1, in Decl.thy*) (* direct subclass *) 

34 
(*subcls , by translation*) (* subclass *) 

35 
(*subclseq, by translation*) (* subclass + identity *) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

36 
implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct implementation *} 
14674  37 
implmt :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* implementation *} 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

38 
widen :: "prog \<Rightarrow> (ty \<times> ty ) set" {* widening *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

39 
narrow :: "prog \<Rightarrow> (ty \<times> ty ) set" {* narrowing *} 
14674  40 
cast :: "prog \<Rightarrow> (ty \<times> ty ) set" {* casting *} 
12854  41 

42 
syntax 

43 

44 
"@subint1" :: "prog => [qtname, qtname] => bool" ("__<:I1_" [71,71,71] 70) 

45 
"@subint" :: "prog => [qtname, qtname] => bool" ("__<=:I _"[71,71,71] 70) 

46 
(* Defined in Decl.thy: 

47 
"@subcls1" :: "prog => [qtname, qtname] => bool" ("__<:C1_" [71,71,71] 70) 

48 
"@subclseq":: "prog => [qtname, qtname] => bool" ("__<=:C _"[71,71,71] 70) 

49 
"@subcls" :: "prog => [qtname, qtname] => bool" ("__<:C _"[71,71,71] 70) 

50 
*) 

51 
"@implmt1" :: "prog => [qtname, qtname] => bool" ("__~>1_" [71,71,71] 70) 

52 
"@implmt" :: "prog => [qtname, qtname] => bool" ("__~>_" [71,71,71] 70) 

53 
"@widen" :: "prog => [ty , ty ] => bool" ("__<=:_" [71,71,71] 70) 

54 
"@narrow" :: "prog => [ty , ty ] => bool" ("__:>_" [71,71,71] 70) 

55 
"@cast" :: "prog => [ty , ty ] => bool" ("__<=:? _"[71,71,71] 70) 

56 

57 
syntax (symbols) 

58 

59 
"@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) 

60 
"@subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) 

61 
(* Defined in Decl.thy: 

62 
\ "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70) 

63 
"@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) 

64 
"@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70) 

65 
*) 

66 
"@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70) 

67 
"@implmt" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70) 

68 
"@widen" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70) 

69 
"@narrow" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70) 

70 
"@cast" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70) 

71 

72 
translations 

73 

74 
"G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G" 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

75 
"G\<turnstile>I \<preceq>I J" == "(I,J) \<in>(subint1 G)^*" {* cf. 9.1.3 *} 
12854  76 
(* Defined in Decl.thy: 
77 
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G" 

78 
"G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*" 

79 
*) 

80 
"G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G" 

81 
"G\<turnstile>C \<leadsto> I" == "(C,I) \<in> implmt G" 

82 
"G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" 

83 
"G\<turnstile>S \<succ> T" == "(S,T) \<in> narrow G" 

84 
"G\<turnstile>S \<preceq>? T" == "(S,T) \<in> cast G" 

85 

86 

87 
section "subclass and subinterface relations" 

88 

89 
(* direct subinterface in Decl.thy, cf. 9.1.3 *) 

90 
(* direct subclass in Decl.thy, cf. 8.1.3 *) 

91 

92 
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard] 

93 

94 
lemma subcls_direct1: 

95 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D" 

96 
apply (auto dest: subcls_direct) 

97 
done 

98 

99 
lemma subcls1I1: 

100 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C\<^sub>1 D" 

101 
apply (auto dest: subcls1I) 

102 
done 

103 

104 
lemma subcls_direct2: 

105 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C D" 

106 
apply (auto dest: subcls1I1) 

107 
done 

108 

109 
lemma subclseq_trans: "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C B; G\<turnstile>B \<preceq>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<preceq>\<^sub>C C" 

110 
by (blast intro: rtrancl_trans) 

111 

112 
lemma subcls_trans: "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C B; G\<turnstile>B \<prec>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<prec>\<^sub>C C" 

113 
by (blast intro: trancl_trans) 

114 

115 
lemma SXcpt_subcls_Throwable_lemma: 

116 
"\<lbrakk>class G (SXcpt xn) = Some xc; 

117 
super xc = (if xn = Throwable then Object else SXcpt Throwable)\<rbrakk> 

118 
\<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" 

119 
apply (case_tac "xn = Throwable") 

120 
apply simp_all 

121 
apply (drule subcls_direct) 

122 
apply (auto dest: sym) 

123 
done 

124 

125 
lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object" 

126 
apply (erule ws_subcls1_induct) 

127 
apply clarsimp 

128 
apply (case_tac "C = Object") 

129 
apply (fast intro: r_into_rtrancl [THEN rtrancl_trans])+ 

130 
done 

131 

132 
lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>\<^sub>C C \<Longrightarrow> C = Object" 

133 
apply (erule rtrancl_induct) 

134 
apply (auto dest: subcls1D) 

135 
done 

136 

137 
lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>\<^sub>C C \<Longrightarrow> False" 

138 
apply (erule trancl_induct) 

139 
apply (auto dest: subcls1D) 

140 
done 

141 

142 
lemma subcls_ObjectI1 [intro!]: 

143 
"\<lbrakk>C \<noteq> Object;is_class G C;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C \<prec>\<^sub>C Object" 

144 
apply (drule (1) subcls_ObjectI) 

145 
apply (auto intro: rtrancl_into_trancl3) 

146 
done 

147 

148 
lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C" 

149 
apply (erule trancl_trans_induct) 

150 
apply (auto dest!: subcls1D) 

151 
done 

152 

153 
lemma subcls_is_class2 [rule_format (no_asm)]: 

154 
"G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" 

155 
apply (erule rtrancl_induct) 

156 
apply (drule_tac [2] subcls1D) 

157 
apply auto 

158 
done 

159 

160 
lemma single_inheritance: 

161 
"\<lbrakk>G\<turnstile>A \<prec>\<^sub>C\<^sub>1 B; G\<turnstile>A \<prec>\<^sub>C\<^sub>1 C\<rbrakk> \<Longrightarrow> B = C" 

162 
by (auto simp add: subcls1_def) 

163 

164 
lemma subcls_compareable: 

165 
"\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C X; G\<turnstile>A \<preceq>\<^sub>C Y 

166 
\<rbrakk> \<Longrightarrow> G\<turnstile>X \<preceq>\<^sub>C Y \<or> G\<turnstile>Y \<preceq>\<^sub>C X" 

167 
by (rule triangle_lemma) (auto intro: single_inheritance) 

168 

169 
lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D; ws_prog G \<rbrakk> 

170 
\<Longrightarrow> C \<noteq> D" 

171 
proof 

172 
assume ws: "ws_prog G" and 

173 
subcls1: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" and 

174 
eq_C_D: "C=D" 

175 
from subcls1 obtain c 

176 
where 

177 
neq_C_Object: "C\<noteq>Object" and 

178 
clsC: "class G C = Some c" and 

179 
super_c: "super c = D" 

180 
by (auto simp add: subcls1_def) 

181 
with super_c subcls1 eq_C_D 

182 
have subcls_super_c_C: "G\<turnstile>super c \<prec>\<^sub>C C" 

183 
by auto 

184 
from ws clsC neq_C_Object 

185 
have "\<not> G\<turnstile>super c \<prec>\<^sub>C C" 

186 
by (auto dest: ws_prog_cdeclD) 

187 
from this subcls_super_c_C 

188 
show "False" 

189 
by (rule notE) 

190 
qed 

191 

192 
lemma no_subcls_Object: "G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> C \<noteq> Object" 

193 
by (erule converse_trancl_induct) (auto dest: subcls1D) 

194 

195 
lemma subcls_acyclic: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C" 

196 
proof  

197 
assume ws: "ws_prog G" 

198 
assume subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D" 

199 
then show ?thesis 

200 
proof (induct rule: converse_trancl_induct) 

201 
fix C 

202 
assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" 

203 
then obtain c where 

204 
"C\<noteq>Object" and 

205 
"class G C = Some c" and 

206 
"super c = D" 

207 
by (auto simp add: subcls1_def) 

208 
with ws 

209 
show "\<not> G\<turnstile>D \<prec>\<^sub>C C" 

210 
by (auto dest: ws_prog_cdeclD) 

211 
next 

212 
fix C Z 

213 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and 

214 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and 

215 
nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z" 

216 
show "\<not> G\<turnstile>D \<prec>\<^sub>C C" 

217 
proof 

218 
assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C" 

219 
show "False" 

220 
proof  

221 
from subcls_D_C subcls1_C_Z 

222 
have "G\<turnstile>D \<prec>\<^sub>C Z" 

223 
by (auto dest: r_into_trancl trancl_trans) 

224 
with nsubcls_D_Z 

225 
show ?thesis 

226 
by (rule notE) 

227 
qed 

228 
qed 

229 
qed 

230 
qed 

231 

232 
lemma subclseq_cases [consumes 1, case_names Eq Subcls]: 

233 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

234 
by (blast intro: rtrancl_cases) 

235 

236 
lemma subclseq_acyclic: 

237 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D" 

238 
by (auto elim: subclseq_cases dest: subcls_acyclic) 

239 

240 
lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> 

241 
\<Longrightarrow> C \<noteq> D" 

242 
proof  

243 
assume ws: "ws_prog G" 

244 
assume subcls: "G\<turnstile>C \<prec>\<^sub>C D" 

245 
then show ?thesis 

246 
proof (induct rule: converse_trancl_induct) 

247 
fix C 

248 
assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" 

249 
with ws 

250 
show "C\<noteq>D" 

251 
by (blast dest: subcls1_irrefl) 

252 
next 

253 
fix C Z 

254 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and 

255 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and 

256 
neq_Z_D: "Z \<noteq> D" 

257 
show "C\<noteq>D" 

258 
proof 

259 
assume eq_C_D: "C=D" 

260 
show "False" 

261 
proof  

262 
from subcls1_C_Z eq_C_D 

263 
have "G\<turnstile>D \<prec>\<^sub>C Z" 

264 
by (auto) 

265 
also 

266 
from subcls_Z_D ws 

267 
have "\<not> G\<turnstile>D \<prec>\<^sub>C Z" 

268 
by (rule subcls_acyclic) 

269 
ultimately 

270 
show ?thesis 

271 
by  (rule notE) 

272 
qed 

273 
qed 

274 
qed 

275 
qed 

276 

277 
lemma invert_subclseq: 

278 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk> 

279 
\<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C" 

280 
proof  

281 
assume ws: "ws_prog G" and 

282 
subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 

283 
show ?thesis 

284 
proof (cases "D=C") 

285 
case True 

286 
with ws 

287 
show ?thesis 

288 
by (auto dest: subcls_irrefl) 

289 
next 

290 
case False 

291 
with subclseq_C_D 

292 
have "G\<turnstile>C \<prec>\<^sub>C D" 

293 
by (blast intro: rtrancl_into_trancl3) 

294 
with ws 

295 
show ?thesis 

296 
by (blast dest: subcls_acyclic) 

297 
qed 

298 
qed 

299 

300 
lemma invert_subcls: 

301 
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> 

302 
\<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C" 

303 
proof  

304 
assume ws: "ws_prog G" and 

305 
subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D" 

306 
then 

307 
have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C" 

308 
by (blast dest: subcls_acyclic) 

309 
show ?thesis 

310 
proof 

311 
assume "G\<turnstile>D \<preceq>\<^sub>C C" 

312 
then show "False" 

313 
proof (cases rule: subclseq_cases) 

314 
case Eq 

315 
with ws subcls_C_D 

316 
show ?thesis 

317 
by (auto dest: subcls_irrefl) 

318 
next 

319 
case Subcls 

320 
with nsubcls_D_C 

321 
show ?thesis 

322 
by blast 

323 
qed 

324 
qed 

325 
qed 

326 

327 
lemma subcls_superD: 

328 
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D" 

329 
proof  

330 
assume clsC: "class G C = Some c" 

331 
assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D" 

332 
then obtain S where 

333 
"G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" and 

334 
subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D" 

335 
by (blast dest: tranclD) 

336 
with clsC 

337 
have "S=super c" 

338 
by (auto dest: subcls1D) 

339 
with subclseq_S_D show ?thesis by simp 

340 
qed 

341 

342 

343 
lemma subclseq_superD: 

344 
"\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C\<noteq>D;class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D" 

345 
proof  

346 
assume neq_C_D: "C\<noteq>D" 

347 
assume clsC: "class G C = Some c" 

348 
assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 

349 
then show ?thesis 

350 
proof (cases rule: subclseq_cases) 

351 
case Eq with neq_C_D show ?thesis by contradiction 

352 
next 

353 
case Subcls 

354 
with clsC show ?thesis by (blast dest: subcls_superD) 

355 
qed 

356 
qed 

357 

358 
section "implementation relation" 

359 

360 
defs 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

361 
{* direct implementation, cf. 8.1.3 *} 
12854  362 
implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}" 
363 

364 
lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))" 

365 
apply (unfold implmt1_def) 

366 
apply auto 

367 
done 

368 

369 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

370 
inductive "implmt G" intros {* cf. 8.1.4 *} 
12854  371 

372 
direct: "G\<turnstile>C\<leadsto>1J \<spacespace>\<spacespace> \<Longrightarrow> G\<turnstile>C\<leadsto>J" 

373 
subint: "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J" 

374 
subcls1: "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C\<^sub>1D; G\<turnstile>D\<leadsto>J \<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J" 

375 

376 
lemma implmtD: "G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> (\<exists>D. G\<turnstile>C\<prec>\<^sub>C\<^sub>1D \<and> G\<turnstile>D\<leadsto>J)" 

377 
apply (erule implmt.induct) 

378 
apply fast+ 

379 
done 

380 

381 
lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R" 

382 
by (auto dest!: implmtD implmt1D subcls1D) 

383 

384 
lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>\<^sub>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K" 

385 
apply (erule rtrancl_induct) 

386 
apply (auto intro: implmt.subcls1) 

387 
done 

388 

389 
lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K" 

390 
apply (erule make_imp, erule implmt.induct) 

391 
apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) 

392 
done 

393 

394 
lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" 

395 
apply (erule implmt.induct) 

396 
apply (blast dest: implmt1D subcls1D)+ 

397 
done 

398 

399 

400 
section "widening relation" 

401 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

402 
inductive "widen G" intros 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

403 
{*widening, viz. method invocation conversion, cf. 5.3 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

404 
i.e. kind of syntactic subtyping *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

405 
refl: "G\<turnstile>T\<preceq>T" {*identity conversion, cf. 5.1.1 *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

406 
subint: "G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" {*wid.ref.conv.,cf. 5.1.4 *} 
12854  407 
int_obj: "G\<turnstile>Iface I\<preceq> Class Object" 
408 
subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D" 

409 
implmt: "G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I" 

410 
null: "G\<turnstile>NT\<preceq> RefT R" 

411 
arr_obj: "G\<turnstile>T.[]\<preceq> Class Object" 

412 
array: "G\<turnstile>RefT S\<preceq>RefT T \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]" 

413 

414 
declare widen.refl [intro!] 

415 
declare widen.intros [simp] 

416 

417 
(* too strong in general: 

418 
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x" 

419 
*) 

420 
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)" 

421 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

422 
by auto 

423 

424 
(* too strong in general: 

425 
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x" 

426 
*) 

427 
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y" 

428 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

429 
by auto 

430 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

431 
text {* 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

432 
These widening lemmata hold in Bali but are to strong for ordinary 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

433 
Java. They would not work for real Java Integral Types, like short, 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

434 
long, int. These lemmata are just for documentation and are not used. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

435 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

436 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

437 
lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

438 
by (ind_cases "G\<turnstile>S\<preceq>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

439 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

440 
lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

441 
by (ind_cases "G\<turnstile>S\<preceq>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

442 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

443 
text {* Specialized versions for booleans also would work for real Java *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

444 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

445 
lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

446 
by (ind_cases "G\<turnstile>S\<preceq>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

447 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

448 
lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

449 
by (ind_cases "G\<turnstile>S\<preceq>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

450 

12854  451 
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t" 
452 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

453 
by auto 

454 

455 
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t" 

456 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

457 
by auto 

458 

459 
lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)" 

460 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

461 
by auto 

462 

463 
lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)" 

464 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

465 
by auto 

466 

467 
lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J" 

468 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

469 
by auto 

470 

471 
lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J" 

472 
apply (rule iffI) 

473 
apply (erule widen_Iface_Iface) 

474 
apply (erule widen.subint) 

475 
done 

476 

477 
lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow> (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)" 

478 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

479 
by auto 

480 

481 
lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)" 

482 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

483 
by auto 

484 

485 
lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm" 

486 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

487 
by auto 

488 

489 
lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm" 

490 
apply (rule iffI) 

491 
apply (erule widen_Class_Class) 

492 
apply (erule widen.subcls) 

493 
done 

494 

495 
lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I" 

496 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

497 
by auto 

498 

499 
lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I" 

500 
apply (rule iffI) 

501 
apply (erule widen_Class_Iface) 

502 
apply (erule widen.implmt) 

503 
done 

504 

505 
lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')" 

506 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

507 
by auto 

508 

509 
lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)" 

510 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

511 
by auto 

512 

513 

514 
lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]" 

515 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

516 
by auto 

517 

518 
lemma widen_ArrayRefT: 

519 
"G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)" 

520 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

521 
by auto 

522 

523 
lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 

524 
"G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'" 

525 
apply (rule iffI) 

526 
apply (drule widen_ArrayRefT) 

527 
apply simp 

528 
apply (erule widen.array) 

529 
done 

530 

531 
lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'" 

532 
apply (drule widen_Array) 

533 
apply auto 

534 
done 

535 

536 
lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object" 

537 
by (auto dest: widen_Array) 

538 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

539 

12854  540 
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT" 
541 
apply (ind_cases "G\<turnstile>S\<preceq>T") 

542 
by auto 

543 

544 
lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object" 

545 
apply (case_tac T) 

546 
apply (auto) 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14674
diff
changeset

547 
apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object") 
12854  548 
apply (auto intro: subcls_ObjectI) 
549 
done 

550 

551 
lemma widen_trans_lemma [rule_format (no_asm)]: 

552 
"\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T" 

553 
apply (erule widen.induct) 

554 
apply safe 

555 
prefer 5 apply (drule widen_RefT) apply clarsimp 

556 
apply (frule_tac [1] widen_Iface) 

557 
apply (frule_tac [2] widen_Class) 

558 
apply (frule_tac [3] widen_Class) 

559 
apply (frule_tac [4] widen_Iface) 

560 
apply (frule_tac [5] widen_Class) 

561 
apply (frule_tac [6] widen_Array) 

562 
apply safe 

563 
apply (rule widen.int_obj) 

564 
prefer 6 apply (drule implmt_is_class) apply simp 

565 
apply (tactic "ALLGOALS (etac thin_rl)") 

566 
prefer 6 apply simp 

567 
apply (rule_tac [9] widen.arr_obj) 

568 
apply (rotate_tac [9] 1) 

569 
apply (frule_tac [9] widen_RefT) 

570 
apply (auto elim!: rtrancl_trans subcls_implmt implmt_subint2) 

571 
done 

572 

573 
lemma ws_widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 

574 
by (auto intro: widen_trans_lemma subcls_ObjectI) 

575 

576 
lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T; 

577 
\<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J; 

578 
\<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D; 

579 
\<forall>I . G\<turnstile>Object\<leadsto>I \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T" 

580 
apply (erule widen.induct) 

581 
apply (auto dest: widen_Iface widen_NT2 widen_Class) 

582 
done 

583 

584 
lemmas subint_antisym = 

585 
subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] 

586 
lemmas subcls_antisym = 

587 
subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] 

588 

589 
lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T" 

590 
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 

591 
subcls_antisym [THEN antisymD]) 

592 

593 
lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object" 

594 
apply (frule widen_Class) 

595 
apply (fast dest: widen_Class_Class widen_Class_Iface) 

596 
done 

597 

598 
constdefs 

599 
widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) 

600 
"G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'" 

601 

602 
lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]" 

603 
apply (unfold widens_def) 

604 
apply auto 

605 
done 

606 

607 
lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)" 

608 
apply (unfold widens_def) 

609 
apply auto 

610 
done 

611 

612 

613 
section "narrowing relation" 

614 

615 
(* all properties of narrowing and casting conversions we actually need *) 

616 
(* these can easily be proven from the definitions below *) 

617 
(* 

618 
rules 

619 
cast_RefT2 "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t" 

620 
cast_PrimT2 "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 

621 
*) 

622 

623 
(* more detailed than necessary for typesafety, see above rules. *) 

624 
inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *) 

625 

626 
subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile> Class D\<succ>Class C" 

627 
implmt: "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile> Class C\<succ>Iface I" 

628 
obj_arr: "G\<turnstile>Class Object\<succ>T.[]" 

629 
int_cls: "G\<turnstile> Iface I\<succ>Class C" 

630 
subint: "imethds G I hidings imethds G J entails 

631 
(\<lambda>(md, mh ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow> 

632 
\<not>G\<turnstile>I\<preceq>I J \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile> Iface I\<succ>Iface J" 

633 
array: "G\<turnstile>RefT S\<succ>RefT T \<spacespace>\<Longrightarrow> G\<turnstile> RefT S.[]\<succ>RefT T.[]" 

634 

635 
(*unused*) 

636 
lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t" 

637 
apply (ind_cases "G\<turnstile>S\<succ>T") 

638 
by auto 

639 

640 
lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t" 

641 
apply (ind_cases "G\<turnstile>S\<succ>T") 

642 
by auto 

643 

644 
(*unused*) 

645 
lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t" 

646 
apply (ind_cases "G\<turnstile>S\<succ>T") 

647 
by auto 

648 

649 
lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> 

650 
\<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 

651 
apply (ind_cases "G\<turnstile>S\<succ>T") 

652 
by auto 

653 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

654 
text {* 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

655 
These narrowing lemmata hold in Bali but are to strong for ordinary 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

656 
Java. They would not work for real Java Integral Types, like short, 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

657 
long, int. These lemmata are just for documentation and are not used. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

658 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

659 
lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

660 
by (ind_cases "G\<turnstile>S\<succ>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

661 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

662 
lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

663 
by (ind_cases "G\<turnstile>S\<succ>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

664 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

665 
text {* Specialized versions for booleans also would work for real Java *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

666 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

667 
lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

668 
by (ind_cases "G\<turnstile>S\<succ>T") simp_all 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

669 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

670 
lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

671 
by (ind_cases "G\<turnstile>S\<succ>T") simp_all 
12854  672 

673 
section "casting relation" 

674 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

675 
inductive "cast G" intros {* casting conversion, cf. 5.5 *} 
12854  676 

677 
widen: "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" 

678 
narrow: "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" 

679 

680 
(*unused*) 

681 
lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t" 

682 
apply (ind_cases "G\<turnstile>S\<preceq>? T") 

683 
by (auto dest: widen_RefT narrow_RefT) 

684 

685 
lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t" 

686 
apply (ind_cases "G\<turnstile>S\<preceq>? T") 

687 
by (auto dest: widen_RefT2 narrow_RefT2) 

688 

689 
(*unused*) 

690 
lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t" 

691 
apply (ind_cases "G\<turnstile>S\<preceq>? T") 

692 
by (auto dest: widen_PrimT narrow_PrimT) 

693 

694 
lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 

695 
apply (ind_cases "G\<turnstile>S\<preceq>? T") 

696 
by (auto dest: widen_PrimT2 narrow_PrimT2) 

697 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

698 
lemma cast_Boolean: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

699 
assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

700 
shows "T=PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

701 
using bool_cast 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

702 
proof (cases) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

703 
case widen 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

704 
hence "G\<turnstile>PrimT Boolean\<preceq> T" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

705 
by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

706 
thus ?thesis by (rule widen_Boolean) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

707 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

708 
case narrow 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

709 
hence "G\<turnstile>PrimT Boolean\<succ>T" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

710 
by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

711 
thus ?thesis by (rule narrow_Boolean) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

712 
qed 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

713 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

714 
lemma cast_Boolean2: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

715 
assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

716 
shows "S = PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

717 
using bool_cast 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

718 
proof (cases) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

719 
case widen 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

720 
hence "G\<turnstile>S\<preceq> PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

721 
by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

722 
thus ?thesis by (rule widen_Boolean2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

723 
next 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

724 
case narrow 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

725 
hence "G\<turnstile>S\<succ>PrimT Boolean" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

726 
by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

727 
thus ?thesis by (rule narrow_Boolean2) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

728 
qed 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset

729 

12854  730 
end 