author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47176  568fdc70e565 
child 58887  38db8ddc0f57 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/TypeRel.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* The relations between Java types *} 

5 

16417  6 
theory TypeRel imports Decl begin 
12854  7 

8 
text {* 

9 
simplifications: 

10 
\begin{itemize} 

11 
\item subinterface, subclass and widening relation includes identity 

12 
\end{itemize} 

13 
improvements over Java Specification 1.0: 

14 
\begin{itemize} 

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

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

17 
relation 

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

19 
\end{itemize} 

20 
design issues: 

21 
\begin{itemize} 

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

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

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

25 
\end{itemize} 

26 
*} 

27 

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

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

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

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

37956  33 

34 
definition 

35 
implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" {* direct implementation *} 

36 
{* direct implementation, cf. 8.1.3 *} 

37 
where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}" 

38 

12854  39 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

40 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

41 
subint1_syntax :: "prog => [qtname, qtname] => bool" ("__<:I1_" [71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

42 
where "GI <:I1 J == (I,J) \<in> subint1 G" 
12854  43 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

44 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

45 
subint_syntax :: "prog => [qtname, qtname] => bool" ("__<=:I _"[71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

46 
where "GI <=:I J == (I,J) \<in>(subint1 G)^*" {* cf. 9.1.3 *} 
12854  47 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

48 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

49 
implmt1_syntax :: "prog => [qtname, qtname] => bool" ("__~>1_" [71,71,71] 70) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

50 
where "GC ~>1 I == (C,I) \<in> implmt1 G" 
12854  51 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

52 
notation (xsymbols) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

53 
subint1_syntax ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

54 
subint_syntax ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

55 
implmt1_syntax ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70) 
12854  56 

57 

58 
section "subclass and subinterface relations" 

59 

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

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

62 

45605  63 
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl] 
12854  64 

65 
lemma subcls_direct1: 

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

67 
apply (auto dest: subcls_direct) 

68 
done 

69 

70 
lemma subcls1I1: 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

71 
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C1 D" 
12854  72 
apply (auto dest: subcls1I) 
73 
done 

74 

75 
lemma subcls_direct2: 

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

77 
apply (auto dest: subcls1I1) 

78 
done 

79 

80 
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" 

81 
by (blast intro: rtrancl_trans) 

82 

83 
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" 

84 
by (blast intro: trancl_trans) 

85 

86 
lemma SXcpt_subcls_Throwable_lemma: 

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

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

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

90 
apply (case_tac "xn = Throwable") 

91 
apply simp_all 

92 
apply (drule subcls_direct) 

93 
apply (auto dest: sym) 

94 
done 

95 

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

97 
apply (erule ws_subcls1_induct) 

98 
apply clarsimp 

99 
apply (case_tac "C = Object") 

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

101 
done 

102 

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

104 
apply (erule rtrancl_induct) 

105 
apply (auto dest: subcls1D) 

106 
done 

107 

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

109 
apply (erule trancl_induct) 

110 
apply (auto dest: subcls1D) 

111 
done 

112 

113 
lemma subcls_ObjectI1 [intro!]: 

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

115 
apply (drule (1) subcls_ObjectI) 

116 
apply (auto intro: rtrancl_into_trancl3) 

117 
done 

118 

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

120 
apply (erule trancl_trans_induct) 

121 
apply (auto dest!: subcls1D) 

122 
done 

123 

124 
lemma subcls_is_class2 [rule_format (no_asm)]: 

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

126 
apply (erule rtrancl_induct) 

127 
apply (drule_tac [2] subcls1D) 

128 
apply auto 

129 
done 

130 

131 
lemma single_inheritance: 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

132 
"\<lbrakk>G\<turnstile>A \<prec>\<^sub>C1 B; G\<turnstile>A \<prec>\<^sub>C1 C\<rbrakk> \<Longrightarrow> B = C" 
12854  133 
by (auto simp add: subcls1_def) 
134 

135 
lemma subcls_compareable: 

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

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

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

139 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

140 
lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C1 D; ws_prog G \<rbrakk> 
12854  141 
\<Longrightarrow> C \<noteq> D" 
142 
proof 

143 
assume ws: "ws_prog G" and 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

144 
subcls1: "G\<turnstile>C \<prec>\<^sub>C1 D" and 
12854  145 
eq_C_D: "C=D" 
146 
from subcls1 obtain c 

147 
where 

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

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

150 
super_c: "super c = D" 

151 
by (auto simp add: subcls1_def) 

152 
with super_c subcls1 eq_C_D 

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

154 
by auto 

155 
from ws clsC neq_C_Object 

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

157 
by (auto dest: ws_prog_cdeclD) 

158 
from this subcls_super_c_C 

159 
show "False" 

160 
by (rule notE) 

161 
qed 

162 

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

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

165 

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

167 
proof  

168 
assume ws: "ws_prog G" 

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

170 
then show ?thesis 

171 
proof (induct rule: converse_trancl_induct) 

172 
fix C 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

173 
assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C1 D" 
12854  174 
then obtain c where 
175 
"C\<noteq>Object" and 

176 
"class G C = Some c" and 

177 
"super c = D" 

178 
by (auto simp add: subcls1_def) 

179 
with ws 

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

181 
by (auto dest: ws_prog_cdeclD) 

182 
next 

183 
fix C Z 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

184 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and 
12854  185 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and 
186 
nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z" 

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

188 
proof 

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

190 
show "False" 

191 
proof  

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

192 
from subcls_D_C subcls1_C_Z 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

193 
have "G\<turnstile>D \<prec>\<^sub>C Z" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

194 
by (auto dest: r_into_trancl trancl_trans) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

195 
with nsubcls_D_Z 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

196 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

197 
by (rule notE) 
12854  198 
qed 
199 
qed 

200 
qed 

201 
qed 

202 

47176  203 
lemma subclseq_cases: 
204 
assumes "G\<turnstile>C \<preceq>\<^sub>C D" 

205 
obtains (Eq) "C = D"  (Subcls) "G\<turnstile>C \<prec>\<^sub>C D" 

206 
using assms by (blast intro: rtrancl_cases) 

12854  207 

208 
lemma subclseq_acyclic: 

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

210 
by (auto elim: subclseq_cases dest: subcls_acyclic) 

211 

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

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

214 
proof  

215 
assume ws: "ws_prog G" 

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

217 
then show ?thesis 

218 
proof (induct rule: converse_trancl_induct) 

219 
fix C 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

220 
assume "G\<turnstile>C \<prec>\<^sub>C1 D" 
12854  221 
with ws 
222 
show "C\<noteq>D" 

223 
by (blast dest: subcls1_irrefl) 

224 
next 

225 
fix C Z 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

226 
assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and 
12854  227 
subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and 
228 
neq_Z_D: "Z \<noteq> D" 

229 
show "C\<noteq>D" 

230 
proof 

231 
assume eq_C_D: "C=D" 

232 
show "False" 

233 
proof  

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

234 
from subcls1_C_Z eq_C_D 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

235 
have "G\<turnstile>D \<prec>\<^sub>C Z" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

236 
by (auto) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

237 
also 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

238 
from subcls_Z_D ws 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

239 
have "\<not> G\<turnstile>D \<prec>\<^sub>C Z" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

240 
by (rule subcls_acyclic) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

241 
ultimately 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

242 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

243 
by  (rule notE) 
12854  244 
qed 
245 
qed 

246 
qed 

247 
qed 

248 

249 
lemma invert_subclseq: 

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

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

252 
proof  

253 
assume ws: "ws_prog G" and 

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

255 
show ?thesis 

256 
proof (cases "D=C") 

257 
case True 

258 
with ws 

259 
show ?thesis 

260 
by (auto dest: subcls_irrefl) 

261 
next 

262 
case False 

263 
with subclseq_C_D 

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

265 
by (blast intro: rtrancl_into_trancl3) 

266 
with ws 

267 
show ?thesis 

268 
by (blast dest: subcls_acyclic) 

269 
qed 

270 
qed 

271 

272 
lemma invert_subcls: 

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

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

275 
proof  

276 
assume ws: "ws_prog G" and 

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

278 
then 

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

280 
by (blast dest: subcls_acyclic) 

281 
show ?thesis 

282 
proof 

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

284 
then show "False" 

285 
proof (cases rule: subclseq_cases) 

286 
case Eq 

287 
with ws subcls_C_D 

288 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

289 
by (auto dest: subcls_irrefl) 
12854  290 
next 
291 
case Subcls 

292 
with nsubcls_D_C 

293 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

294 
by blast 
12854  295 
qed 
296 
qed 

297 
qed 

298 

299 
lemma subcls_superD: 

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

301 
proof  

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

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

304 
then obtain S where 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

305 
"G\<turnstile>C \<prec>\<^sub>C1 S" and 
12854  306 
subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D" 
307 
by (blast dest: tranclD) 

308 
with clsC 

309 
have "S=super c" 

310 
by (auto dest: subcls1D) 

311 
with subclseq_S_D show ?thesis by simp 

312 
qed 

313 

314 

315 
lemma subclseq_superD: 

316 
"\<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" 

317 
proof  

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

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

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

321 
then show ?thesis 

322 
proof (cases rule: subclseq_cases) 

323 
case Eq with neq_C_D show ?thesis by contradiction 

324 
next 

325 
case Subcls 

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

327 
qed 

328 
qed 

329 

330 
section "implementation relation" 

331 

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

333 
apply (unfold implmt1_def) 

334 
apply auto 

335 
done 

336 

23747  337 
inductive {* implementation, cf. 8.1.4 *} 
21765  338 
implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70) 
339 
for G :: prog 

340 
where 

46212  341 
direct: "G\<turnstile>C\<leadsto>1J \<Longrightarrow> G\<turnstile>C\<leadsto>J" 
342 
 subint: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>C\<leadsto>J" 

343 
 subcls1: "G\<turnstile>C\<prec>\<^sub>C1D \<Longrightarrow> G\<turnstile>D\<leadsto>J \<Longrightarrow> G\<turnstile>C\<leadsto>J" 

12854  344 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

345 
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>C1D \<and> G\<turnstile>D\<leadsto>J)" 
12854  346 
apply (erule implmt.induct) 
347 
apply fast+ 

348 
done 

349 

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

351 
by (auto dest!: implmtD implmt1D subcls1D) 

352 

353 
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" 

354 
apply (erule rtrancl_induct) 

355 
apply (auto intro: implmt.subcls1) 

356 
done 

357 

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

24038  359 
apply (erule rev_mp, erule implmt.induct) 
12854  360 
apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) 
361 
done 

362 

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

364 
apply (erule implmt.induct) 

18447  365 
apply (auto dest: implmt1D subcls1D) 
12854  366 
done 
367 

368 

369 
section "widening relation" 

370 

23747  371 
inductive 
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

372 
{*widening, viz. method invocation conversion, cf. 5.3 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

373 
i.e. kind of syntactic subtyping *} 
21765  374 
widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70) 
375 
for G :: prog 

376 
where 

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

377 
refl: "G\<turnstile>T\<preceq>T" {*identity conversion, cf. 5.1.1 *} 
21765  378 
 subint: "G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" {*wid.ref.conv.,cf. 5.1.4 *} 
379 
 int_obj: "G\<turnstile>Iface I\<preceq> Class Object" 

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

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

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

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

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

12854  385 

386 
declare widen.refl [intro!] 

387 
declare widen.intros [simp] 

388 

389 
(* too strong in general: 

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

391 
*) 

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

23747  393 
apply (ind_cases "G\<turnstile>PrimT x\<preceq>T") 
12854  394 
by auto 
395 

396 
(* too strong in general: 

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

398 
*) 

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

23747  400 
apply (ind_cases "G\<turnstile>S\<preceq>PrimT x") 
12854  401 
by auto 
402 

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

403 
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

404 
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

405 
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

406 
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

407 
*} 
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

408 

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

409 
lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x" 
23747  410 
by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all 
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

411 

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

412 
lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x" 
23747  413 
by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all 
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

414 

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

415 
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

416 

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

417 
lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean" 
23747  418 
by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all 
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

419 

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

420 
lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean" 
23747  421 
by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all 
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

422 

12854  423 
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t" 
23747  424 
apply (ind_cases "G\<turnstile>RefT R\<preceq>T") 
12854  425 
by auto 
426 

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

23747  428 
apply (ind_cases "G\<turnstile>S\<preceq>RefT R") 
12854  429 
by auto 
430 

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

23747  432 
apply (ind_cases "G\<turnstile>Iface I\<preceq>T") 
12854  433 
by auto 
434 

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

23747  436 
apply (ind_cases "G\<turnstile>S\<preceq> Iface J") 
12854  437 
by auto 
438 

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

23747  440 
apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J") 
12854  441 
by auto 
442 

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

444 
apply (rule iffI) 

445 
apply (erule widen_Iface_Iface) 

446 
apply (erule widen.subint) 

447 
done 

448 

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

23747  450 
apply (ind_cases "G\<turnstile>Class C\<preceq>T") 
12854  451 
by auto 
452 

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

23747  454 
apply (ind_cases "G\<turnstile>S\<preceq> Class C") 
12854  455 
by auto 
456 

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

23747  458 
apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm") 
12854  459 
by auto 
460 

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

462 
apply (rule iffI) 

463 
apply (erule widen_Class_Class) 

464 
apply (erule widen.subcls) 

465 
done 

466 

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

23747  468 
apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I") 
12854  469 
by auto 
470 

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

472 
apply (rule iffI) 

473 
apply (erule widen_Class_Iface) 

474 
apply (erule widen.implmt) 

475 
done 

476 

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

23747  478 
apply (ind_cases "G\<turnstile>S.[]\<preceq>T") 
12854  479 
by auto 
480 

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

23747  482 
apply (ind_cases "G\<turnstile>S\<preceq>T.[]") 
12854  483 
by auto 
484 

485 

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

23747  487 
apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T") 
12854  488 
by auto 
489 

490 
lemma widen_ArrayRefT: 

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

23747  492 
apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T") 
12854  493 
by auto 
494 

495 
lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 

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

497 
apply (rule iffI) 

498 
apply (drule widen_ArrayRefT) 

499 
apply simp 

500 
apply (erule widen.array) 

501 
done 

502 

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

504 
apply (drule widen_Array) 

505 
apply auto 

506 
done 

507 

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

509 
by (auto dest: widen_Array) 

510 

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

511 

12854  512 
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT" 
23747  513 
apply (ind_cases "G\<turnstile>S\<preceq>NT") 
12854  514 
by auto 
515 

38541  516 
lemma widen_Object: 
517 
assumes "isrtype G T" and "ws_prog G" 

518 
shows "G\<turnstile>RefT T \<preceq> Class Object" 

519 
proof (cases T) 

520 
case (ClassT C) with assms have "G\<turnstile>C\<preceq>\<^sub>C Object" by (auto intro: subcls_ObjectI) 

521 
with ClassT show ?thesis by auto 

522 
qed simp_all 

12854  523 

524 
lemma widen_trans_lemma [rule_format (no_asm)]: 

525 
"\<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" 

526 
apply (erule widen.induct) 

527 
apply safe 

528 
prefer 5 apply (drule widen_RefT) apply clarsimp 

529 
apply (frule_tac [1] widen_Iface) 

530 
apply (frule_tac [2] widen_Class) 

531 
apply (frule_tac [3] widen_Class) 

532 
apply (frule_tac [4] widen_Iface) 

533 
apply (frule_tac [5] widen_Class) 

534 
apply (frule_tac [6] widen_Array) 

535 
apply safe 

536 
apply (rule widen.int_obj) 

537 
prefer 6 apply (drule implmt_is_class) apply simp 

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

539 
prefer 6 apply simp 

540 
apply (rule_tac [9] widen.arr_obj) 

541 
apply (rotate_tac [9] 1) 

542 
apply (frule_tac [9] widen_RefT) 

543 
apply (auto elim!: rtrancl_trans subcls_implmt implmt_subint2) 

544 
done 

545 

546 
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" 

547 
by (auto intro: widen_trans_lemma subcls_ObjectI) 

548 

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

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

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

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

553 
apply (erule widen.induct) 

554 
apply (auto dest: widen_Iface widen_NT2 widen_Class) 

555 
done 

556 

557 
lemmas subint_antisym = 

45605  558 
subint1_acyclic [THEN acyclic_impl_antisym_rtrancl] 
12854  559 
lemmas subcls_antisym = 
45605  560 
subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl] 
12854  561 

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

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

564 
subcls_antisym [THEN antisymD]) 

565 

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

567 
apply (frule widen_Class) 

568 
apply (fast dest: widen_Class_Class widen_Class_Iface) 

569 
done 

570 

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

573 
where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'" 

12854  574 

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

576 
apply (unfold widens_def) 

577 
apply auto 

578 
done 

579 

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

581 
apply (unfold widens_def) 

582 
apply auto 

583 
done 

584 

585 

586 
section "narrowing relation" 

587 

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

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

590 
(* 

591 
rules 

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

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

594 
*) 

595 

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

23747  597 
inductive {* narrowing reference conversion, cf. 5.1.5 *} 
21765  598 
narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70) 
599 
for G :: prog 

600 
where 

12854  601 
subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile> Class D\<succ>Class C" 
21765  602 
 implmt: "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile> Class C\<succ>Iface I" 
603 
 obj_arr: "G\<turnstile>Class Object\<succ>T.[]" 

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

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

46212  606 
(\<lambda>(md, mh ) (md',mh'). G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow> 
607 
\<not>G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile> Iface I\<succ>Iface J" 

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

12854  609 

610 
(*unused*) 

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

23747  612 
apply (ind_cases "G\<turnstile>RefT R\<succ>T") 
12854  613 
by auto 
614 

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

23747  616 
apply (ind_cases "G\<turnstile>S\<succ>RefT R") 
12854  617 
by auto 
618 

619 
(*unused*) 

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

23747  621 
by (ind_cases "G\<turnstile>PrimT pt\<succ>T") 
12854  622 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24783
diff
changeset

624 
\<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" 
23747  625 
by (ind_cases "G\<turnstile>S\<succ>PrimT pt") 
12854  626 

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

627 
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

628 
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

629 
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

630 
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

631 
*} 
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

632 
lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt" 
23747  633 
by (ind_cases "G\<turnstile>PrimT pt\<succ>T") 
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

634 

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

635 
lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt" 
23747  636 
by (ind_cases "G\<turnstile>S\<succ>PrimT pt") 
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

637 

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

638 
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

639 

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

640 
lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean" 
23747  641 
by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T") 
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

642 

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

643 
lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean" 
23747  644 
by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean") 
12854  645 

646 
section "casting relation" 

647 

23747  648 
inductive {* casting conversion, cf. 5.5 *} 
21765  649 
cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70) 
650 
for G :: prog 

651 
where 

12854  652 
widen: "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" 
21765  653 
 narrow: "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" 
12854  654 

655 
(*unused*) 

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

23747  657 
apply (ind_cases "G\<turnstile>RefT R\<preceq>? T") 
12854  658 
by (auto dest: widen_RefT narrow_RefT) 
659 

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

23747  661 
apply (ind_cases "G\<turnstile>S\<preceq>? RefT R") 
12854  662 
by (auto dest: widen_RefT2 narrow_RefT2) 
663 

664 
(*unused*) 

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

23747  666 
apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T") 
12854  667 
by (auto dest: widen_PrimT narrow_PrimT) 
668 

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

23747  670 
apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt") 
12854  671 
by (auto dest: widen_PrimT2 narrow_PrimT2) 
672 

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

673 
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

674 
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

675 
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

676 
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

677 
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

678 
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

679 
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

680 
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

681 
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

682 
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

683 
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

684 
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

685 
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

686 
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

687 
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

688 

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

689 
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

690 
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

691 
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

692 
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

693 
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

694 
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

695 
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

696 
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

697 
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

698 
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

699 
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

700 
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

701 
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

702 
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

703 
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

704 

12854  705 
end 