|
1 (* Title: isabelle/Bali/TypeRel.thy |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1997 Technische Universitaet Muenchen |
|
5 *) |
|
6 header {* The relations between Java types *} |
|
7 |
|
8 theory TypeRel = Decl: |
|
9 |
|
10 text {* |
|
11 simplifications: |
|
12 \begin{itemize} |
|
13 \item subinterface, subclass and widening relation includes identity |
|
14 \end{itemize} |
|
15 improvements over Java Specification 1.0: |
|
16 \begin{itemize} |
|
17 \item narrowing reference conversion also in cases where the return types of a |
|
18 pair of methods common to both types are in widening (rather identity) |
|
19 relation |
|
20 \item one could add similar constraints also for other cases |
|
21 \end{itemize} |
|
22 design issues: |
|
23 \begin{itemize} |
|
24 \item the type relations do not require @{text is_type} for their arguments |
|
25 \item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class} |
|
26 for their first arguments, which is required for their finiteness |
|
27 \end{itemize} |
|
28 *} |
|
29 |
|
30 consts |
|
31 |
|
32 (*subint1, in Decl.thy*) (* direct subinterface *) |
|
33 (*subint , by translation*) (* subinterface (+ identity) *) |
|
34 (*subcls1, in Decl.thy*) (* direct subclass *) |
|
35 (*subcls , by translation*) (* subclass *) |
|
36 (*subclseq, by translation*) (* subclass + identity *) |
|
37 implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" (* direct implementation *) |
|
38 implmt :: "prog \<Rightarrow> (qtname \<times> qtname) set" (* implementation *) |
|
39 widen :: "prog \<Rightarrow> (ty \<times> ty ) set" (* widening *) |
|
40 narrow :: "prog \<Rightarrow> (ty \<times> ty ) set" (* narrowing *) |
|
41 cast :: "prog \<Rightarrow> (ty \<times> ty ) set" (* casting *) |
|
42 |
|
43 syntax |
|
44 |
|
45 "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70) |
|
46 "@subint" :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70) |
|
47 (* Defined in Decl.thy: |
|
48 "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70) |
|
49 "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70) |
|
50 "@subcls" :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70) |
|
51 *) |
|
52 "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_" [71,71,71] 70) |
|
53 "@implmt" :: "prog => [qtname, qtname] => bool" ("_|-_~>_" [71,71,71] 70) |
|
54 "@widen" :: "prog => [ty , ty ] => bool" ("_|-_<=:_" [71,71,71] 70) |
|
55 "@narrow" :: "prog => [ty , ty ] => bool" ("_|-_:>_" [71,71,71] 70) |
|
56 "@cast" :: "prog => [ty , ty ] => bool" ("_|-_<=:? _"[71,71,71] 70) |
|
57 |
|
58 syntax (symbols) |
|
59 |
|
60 "@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_" [71,71,71] 70) |
|
61 "@subint" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _" [71,71,71] 70) |
|
62 (* Defined in Decl.thy: |
|
63 \ "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_" [71,71,71] 70) |
|
64 "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _" [71,71,71] 70) |
|
65 "@subcls" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _" [71,71,71] 70) |
|
66 *) |
|
67 "@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_" [71,71,71] 70) |
|
68 "@implmt" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70) |
|
69 "@widen" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70) |
|
70 "@narrow" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70) |
|
71 "@cast" :: "prog \<Rightarrow> [ty , ty ] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70) |
|
72 |
|
73 translations |
|
74 |
|
75 "G\<turnstile>I \<prec>I1 J" == "(I,J) \<in> subint1 G" |
|
76 "G\<turnstile>I \<preceq>I J" == "(I,J) \<in>(subint1 G)^*" (* cf. 9.1.3 *) |
|
77 (* Defined in Decl.thy: |
|
78 "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G" |
|
79 "G\<turnstile>C \<preceq>\<^sub>C D" == "(C,D) \<in>(subcls1 G)^*" |
|
80 *) |
|
81 "G\<turnstile>C \<leadsto>1 I" == "(C,I) \<in> implmt1 G" |
|
82 "G\<turnstile>C \<leadsto> I" == "(C,I) \<in> implmt G" |
|
83 "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" |
|
84 "G\<turnstile>S \<succ> T" == "(S,T) \<in> narrow G" |
|
85 "G\<turnstile>S \<preceq>? T" == "(S,T) \<in> cast G" |
|
86 |
|
87 |
|
88 section "subclass and subinterface relations" |
|
89 |
|
90 (* direct subinterface in Decl.thy, cf. 9.1.3 *) |
|
91 (* direct subclass in Decl.thy, cf. 8.1.3 *) |
|
92 |
|
93 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard] |
|
94 |
|
95 lemma subcls_direct1: |
|
96 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D" |
|
97 apply (auto dest: subcls_direct) |
|
98 done |
|
99 |
|
100 lemma subcls1I1: |
|
101 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C\<^sub>1 D" |
|
102 apply (auto dest: subcls1I) |
|
103 done |
|
104 |
|
105 lemma subcls_direct2: |
|
106 "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C D" |
|
107 apply (auto dest: subcls1I1) |
|
108 done |
|
109 |
|
110 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" |
|
111 by (blast intro: rtrancl_trans) |
|
112 |
|
113 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" |
|
114 by (blast intro: trancl_trans) |
|
115 |
|
116 lemma SXcpt_subcls_Throwable_lemma: |
|
117 "\<lbrakk>class G (SXcpt xn) = Some xc; |
|
118 super xc = (if xn = Throwable then Object else SXcpt Throwable)\<rbrakk> |
|
119 \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" |
|
120 apply (case_tac "xn = Throwable") |
|
121 apply simp_all |
|
122 apply (drule subcls_direct) |
|
123 apply (auto dest: sym) |
|
124 done |
|
125 |
|
126 lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object" |
|
127 apply (erule ws_subcls1_induct) |
|
128 apply clarsimp |
|
129 apply (case_tac "C = Object") |
|
130 apply (fast intro: r_into_rtrancl [THEN rtrancl_trans])+ |
|
131 done |
|
132 |
|
133 lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>\<^sub>C C \<Longrightarrow> C = Object" |
|
134 apply (erule rtrancl_induct) |
|
135 apply (auto dest: subcls1D) |
|
136 done |
|
137 |
|
138 lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>\<^sub>C C \<Longrightarrow> False" |
|
139 apply (erule trancl_induct) |
|
140 apply (auto dest: subcls1D) |
|
141 done |
|
142 |
|
143 lemma subcls_ObjectI1 [intro!]: |
|
144 "\<lbrakk>C \<noteq> Object;is_class G C;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C \<prec>\<^sub>C Object" |
|
145 apply (drule (1) subcls_ObjectI) |
|
146 apply (auto intro: rtrancl_into_trancl3) |
|
147 done |
|
148 |
|
149 lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C" |
|
150 apply (erule trancl_trans_induct) |
|
151 apply (auto dest!: subcls1D) |
|
152 done |
|
153 |
|
154 lemma subcls_is_class2 [rule_format (no_asm)]: |
|
155 "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" |
|
156 apply (erule rtrancl_induct) |
|
157 apply (drule_tac [2] subcls1D) |
|
158 apply auto |
|
159 done |
|
160 |
|
161 lemma single_inheritance: |
|
162 "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C\<^sub>1 B; G\<turnstile>A \<prec>\<^sub>C\<^sub>1 C\<rbrakk> \<Longrightarrow> B = C" |
|
163 by (auto simp add: subcls1_def) |
|
164 |
|
165 lemma subcls_compareable: |
|
166 "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C X; G\<turnstile>A \<preceq>\<^sub>C Y |
|
167 \<rbrakk> \<Longrightarrow> G\<turnstile>X \<preceq>\<^sub>C Y \<or> G\<turnstile>Y \<preceq>\<^sub>C X" |
|
168 by (rule triangle_lemma) (auto intro: single_inheritance) |
|
169 |
|
170 lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D; ws_prog G \<rbrakk> |
|
171 \<Longrightarrow> C \<noteq> D" |
|
172 proof |
|
173 assume ws: "ws_prog G" and |
|
174 subcls1: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" and |
|
175 eq_C_D: "C=D" |
|
176 from subcls1 obtain c |
|
177 where |
|
178 neq_C_Object: "C\<noteq>Object" and |
|
179 clsC: "class G C = Some c" and |
|
180 super_c: "super c = D" |
|
181 by (auto simp add: subcls1_def) |
|
182 with super_c subcls1 eq_C_D |
|
183 have subcls_super_c_C: "G\<turnstile>super c \<prec>\<^sub>C C" |
|
184 by auto |
|
185 from ws clsC neq_C_Object |
|
186 have "\<not> G\<turnstile>super c \<prec>\<^sub>C C" |
|
187 by (auto dest: ws_prog_cdeclD) |
|
188 from this subcls_super_c_C |
|
189 show "False" |
|
190 by (rule notE) |
|
191 qed |
|
192 |
|
193 lemma no_subcls_Object: "G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> C \<noteq> Object" |
|
194 by (erule converse_trancl_induct) (auto dest: subcls1D) |
|
195 |
|
196 lemma subcls_acyclic: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C" |
|
197 proof - |
|
198 assume ws: "ws_prog G" |
|
199 assume subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D" |
|
200 then show ?thesis |
|
201 proof (induct rule: converse_trancl_induct) |
|
202 fix C |
|
203 assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" |
|
204 then obtain c where |
|
205 "C\<noteq>Object" and |
|
206 "class G C = Some c" and |
|
207 "super c = D" |
|
208 by (auto simp add: subcls1_def) |
|
209 with ws |
|
210 show "\<not> G\<turnstile>D \<prec>\<^sub>C C" |
|
211 by (auto dest: ws_prog_cdeclD) |
|
212 next |
|
213 fix C Z |
|
214 assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and |
|
215 subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and |
|
216 nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z" |
|
217 show "\<not> G\<turnstile>D \<prec>\<^sub>C C" |
|
218 proof |
|
219 assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C" |
|
220 show "False" |
|
221 proof - |
|
222 from subcls_D_C subcls1_C_Z |
|
223 have "G\<turnstile>D \<prec>\<^sub>C Z" |
|
224 by (auto dest: r_into_trancl trancl_trans) |
|
225 with nsubcls_D_Z |
|
226 show ?thesis |
|
227 by (rule notE) |
|
228 qed |
|
229 qed |
|
230 qed |
|
231 qed |
|
232 |
|
233 lemma subclseq_cases [consumes 1, case_names Eq Subcls]: |
|
234 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
235 by (blast intro: rtrancl_cases) |
|
236 |
|
237 lemma subclseq_acyclic: |
|
238 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D" |
|
239 by (auto elim: subclseq_cases dest: subcls_acyclic) |
|
240 |
|
241 lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> |
|
242 \<Longrightarrow> C \<noteq> D" |
|
243 proof - |
|
244 assume ws: "ws_prog G" |
|
245 assume subcls: "G\<turnstile>C \<prec>\<^sub>C D" |
|
246 then show ?thesis |
|
247 proof (induct rule: converse_trancl_induct) |
|
248 fix C |
|
249 assume "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" |
|
250 with ws |
|
251 show "C\<noteq>D" |
|
252 by (blast dest: subcls1_irrefl) |
|
253 next |
|
254 fix C Z |
|
255 assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 Z" and |
|
256 subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and |
|
257 neq_Z_D: "Z \<noteq> D" |
|
258 show "C\<noteq>D" |
|
259 proof |
|
260 assume eq_C_D: "C=D" |
|
261 show "False" |
|
262 proof - |
|
263 from subcls1_C_Z eq_C_D |
|
264 have "G\<turnstile>D \<prec>\<^sub>C Z" |
|
265 by (auto) |
|
266 also |
|
267 from subcls_Z_D ws |
|
268 have "\<not> G\<turnstile>D \<prec>\<^sub>C Z" |
|
269 by (rule subcls_acyclic) |
|
270 ultimately |
|
271 show ?thesis |
|
272 by - (rule notE) |
|
273 qed |
|
274 qed |
|
275 qed |
|
276 qed |
|
277 |
|
278 lemma invert_subclseq: |
|
279 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk> |
|
280 \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C" |
|
281 proof - |
|
282 assume ws: "ws_prog G" and |
|
283 subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" |
|
284 show ?thesis |
|
285 proof (cases "D=C") |
|
286 case True |
|
287 with ws |
|
288 show ?thesis |
|
289 by (auto dest: subcls_irrefl) |
|
290 next |
|
291 case False |
|
292 with subclseq_C_D |
|
293 have "G\<turnstile>C \<prec>\<^sub>C D" |
|
294 by (blast intro: rtrancl_into_trancl3) |
|
295 with ws |
|
296 show ?thesis |
|
297 by (blast dest: subcls_acyclic) |
|
298 qed |
|
299 qed |
|
300 |
|
301 lemma invert_subcls: |
|
302 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> |
|
303 \<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C" |
|
304 proof - |
|
305 assume ws: "ws_prog G" and |
|
306 subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D" |
|
307 then |
|
308 have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C" |
|
309 by (blast dest: subcls_acyclic) |
|
310 show ?thesis |
|
311 proof |
|
312 assume "G\<turnstile>D \<preceq>\<^sub>C C" |
|
313 then show "False" |
|
314 proof (cases rule: subclseq_cases) |
|
315 case Eq |
|
316 with ws subcls_C_D |
|
317 show ?thesis |
|
318 by (auto dest: subcls_irrefl) |
|
319 next |
|
320 case Subcls |
|
321 with nsubcls_D_C |
|
322 show ?thesis |
|
323 by blast |
|
324 qed |
|
325 qed |
|
326 qed |
|
327 |
|
328 lemma subcls_superD: |
|
329 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D" |
|
330 proof - |
|
331 assume clsC: "class G C = Some c" |
|
332 assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D" |
|
333 then obtain S where |
|
334 "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S" and |
|
335 subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D" |
|
336 by (blast dest: tranclD) |
|
337 with clsC |
|
338 have "S=super c" |
|
339 by (auto dest: subcls1D) |
|
340 with subclseq_S_D show ?thesis by simp |
|
341 qed |
|
342 |
|
343 |
|
344 lemma subclseq_superD: |
|
345 "\<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" |
|
346 proof - |
|
347 assume neq_C_D: "C\<noteq>D" |
|
348 assume clsC: "class G C = Some c" |
|
349 assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" |
|
350 then show ?thesis |
|
351 proof (cases rule: subclseq_cases) |
|
352 case Eq with neq_C_D show ?thesis by contradiction |
|
353 next |
|
354 case Subcls |
|
355 with clsC show ?thesis by (blast dest: subcls_superD) |
|
356 qed |
|
357 qed |
|
358 |
|
359 section "implementation relation" |
|
360 |
|
361 defs |
|
362 (* direct implementation, cf. 8.1.3 *) |
|
363 implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}" |
|
364 |
|
365 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))" |
|
366 apply (unfold implmt1_def) |
|
367 apply auto |
|
368 done |
|
369 |
|
370 |
|
371 inductive "implmt G" intros (* cf. 8.1.4 *) |
|
372 |
|
373 direct: "G\<turnstile>C\<leadsto>1J \<spacespace>\<spacespace> \<Longrightarrow> G\<turnstile>C\<leadsto>J" |
|
374 subint: "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J" |
|
375 subcls1: "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C\<^sub>1D; G\<turnstile>D\<leadsto>J \<rbrakk> \<Longrightarrow> G\<turnstile>C\<leadsto>J" |
|
376 |
|
377 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)" |
|
378 apply (erule implmt.induct) |
|
379 apply fast+ |
|
380 done |
|
381 |
|
382 lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R" |
|
383 by (auto dest!: implmtD implmt1D subcls1D) |
|
384 |
|
385 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" |
|
386 apply (erule rtrancl_induct) |
|
387 apply (auto intro: implmt.subcls1) |
|
388 done |
|
389 |
|
390 lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K" |
|
391 apply (erule make_imp, erule implmt.induct) |
|
392 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1) |
|
393 done |
|
394 |
|
395 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C" |
|
396 apply (erule implmt.induct) |
|
397 apply (blast dest: implmt1D subcls1D)+ |
|
398 done |
|
399 |
|
400 |
|
401 section "widening relation" |
|
402 |
|
403 inductive "widen G" intros(*widening, viz. method invocation conversion, cf. 5.3 |
|
404 i.e. kind of syntactic subtyping *) |
|
405 refl: "G\<turnstile>T\<preceq>T"(*identity conversion, cf. 5.1.1 *) |
|
406 subint: "G\<turnstile>I\<preceq>I J \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J"(*wid.ref.conv.,cf. 5.1.4 *) |
|
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 |
|
431 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t" |
|
432 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
433 by auto |
|
434 |
|
435 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t" |
|
436 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
437 by auto |
|
438 |
|
439 lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)" |
|
440 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
441 by auto |
|
442 |
|
443 lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)" |
|
444 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
445 by auto |
|
446 |
|
447 lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J" |
|
448 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
449 by auto |
|
450 |
|
451 lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J" |
|
452 apply (rule iffI) |
|
453 apply (erule widen_Iface_Iface) |
|
454 apply (erule widen.subint) |
|
455 done |
|
456 |
|
457 lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow> (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)" |
|
458 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
459 by auto |
|
460 |
|
461 lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)" |
|
462 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
463 by auto |
|
464 |
|
465 lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm" |
|
466 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
467 by auto |
|
468 |
|
469 lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm" |
|
470 apply (rule iffI) |
|
471 apply (erule widen_Class_Class) |
|
472 apply (erule widen.subcls) |
|
473 done |
|
474 |
|
475 lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I" |
|
476 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
477 by auto |
|
478 |
|
479 lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I" |
|
480 apply (rule iffI) |
|
481 apply (erule widen_Class_Iface) |
|
482 apply (erule widen.implmt) |
|
483 done |
|
484 |
|
485 lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')" |
|
486 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
487 by auto |
|
488 |
|
489 lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)" |
|
490 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
491 by auto |
|
492 |
|
493 |
|
494 lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]" |
|
495 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
496 by auto |
|
497 |
|
498 lemma widen_ArrayRefT: |
|
499 "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)" |
|
500 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
501 by auto |
|
502 |
|
503 lemma widen_ArrayRefT_ArrayRefT_eq [simp]: |
|
504 "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'" |
|
505 apply (rule iffI) |
|
506 apply (drule widen_ArrayRefT) |
|
507 apply simp |
|
508 apply (erule widen.array) |
|
509 done |
|
510 |
|
511 lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'" |
|
512 apply (drule widen_Array) |
|
513 apply auto |
|
514 done |
|
515 |
|
516 lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object" |
|
517 by (auto dest: widen_Array) |
|
518 |
|
519 (* |
|
520 qed_typerel "widen_NT2" "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT" |
|
521 [prove_widen_lemma "G\<turnstile>S\<preceq>T \<Longrightarrow> T = NT \<longrightarrow> S = NT"] |
|
522 *) |
|
523 lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT" |
|
524 apply (ind_cases "G\<turnstile>S\<preceq>T") |
|
525 by auto |
|
526 |
|
527 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object" |
|
528 apply (case_tac T) |
|
529 apply (auto) |
|
530 apply (subgoal_tac "G\<turnstile>pid_field_type\<preceq>\<^sub>C Object") |
|
531 apply (auto intro: subcls_ObjectI) |
|
532 done |
|
533 |
|
534 lemma widen_trans_lemma [rule_format (no_asm)]: |
|
535 "\<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" |
|
536 apply (erule widen.induct) |
|
537 apply safe |
|
538 prefer 5 apply (drule widen_RefT) apply clarsimp |
|
539 apply (frule_tac [1] widen_Iface) |
|
540 apply (frule_tac [2] widen_Class) |
|
541 apply (frule_tac [3] widen_Class) |
|
542 apply (frule_tac [4] widen_Iface) |
|
543 apply (frule_tac [5] widen_Class) |
|
544 apply (frule_tac [6] widen_Array) |
|
545 apply safe |
|
546 apply (rule widen.int_obj) |
|
547 prefer 6 apply (drule implmt_is_class) apply simp |
|
548 apply (tactic "ALLGOALS (etac thin_rl)") |
|
549 prefer 6 apply simp |
|
550 apply (rule_tac [9] widen.arr_obj) |
|
551 apply (rotate_tac [9] -1) |
|
552 apply (frule_tac [9] widen_RefT) |
|
553 apply (auto elim!: rtrancl_trans subcls_implmt implmt_subint2) |
|
554 done |
|
555 |
|
556 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" |
|
557 by (auto intro: widen_trans_lemma subcls_ObjectI) |
|
558 |
|
559 lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T; |
|
560 \<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J; |
|
561 \<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D; |
|
562 \<forall>I . G\<turnstile>Object\<leadsto>I \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T" |
|
563 apply (erule widen.induct) |
|
564 apply (auto dest: widen_Iface widen_NT2 widen_Class) |
|
565 done |
|
566 |
|
567 lemmas subint_antisym = |
|
568 subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] |
|
569 lemmas subcls_antisym = |
|
570 subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard] |
|
571 |
|
572 lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T" |
|
573 by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] |
|
574 subcls_antisym [THEN antisymD]) |
|
575 |
|
576 lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object" |
|
577 apply (frule widen_Class) |
|
578 apply (fast dest: widen_Class_Class widen_Class_Iface) |
|
579 done |
|
580 |
|
581 constdefs |
|
582 widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) |
|
583 "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'" |
|
584 |
|
585 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]" |
|
586 apply (unfold widens_def) |
|
587 apply auto |
|
588 done |
|
589 |
|
590 lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)" |
|
591 apply (unfold widens_def) |
|
592 apply auto |
|
593 done |
|
594 |
|
595 |
|
596 section "narrowing relation" |
|
597 |
|
598 (* all properties of narrowing and casting conversions we actually need *) |
|
599 (* these can easily be proven from the definitions below *) |
|
600 (* |
|
601 rules |
|
602 cast_RefT2 "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t" |
|
603 cast_PrimT2 "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" |
|
604 *) |
|
605 |
|
606 (* more detailed than necessary for type-safety, see above rules. *) |
|
607 inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *) |
|
608 |
|
609 subcls: "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile> Class D\<succ>Class C" |
|
610 implmt: "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile> Class C\<succ>Iface I" |
|
611 obj_arr: "G\<turnstile>Class Object\<succ>T.[]" |
|
612 int_cls: "G\<turnstile> Iface I\<succ>Class C" |
|
613 subint: "imethds G I hidings imethds G J entails |
|
614 (\<lambda>(md, mh ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow> |
|
615 \<not>G\<turnstile>I\<preceq>I J \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile> Iface I\<succ>Iface J" |
|
616 array: "G\<turnstile>RefT S\<succ>RefT T \<spacespace>\<Longrightarrow> G\<turnstile> RefT S.[]\<succ>RefT T.[]" |
|
617 |
|
618 (*unused*) |
|
619 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t" |
|
620 apply (ind_cases "G\<turnstile>S\<succ>T") |
|
621 by auto |
|
622 |
|
623 lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t" |
|
624 apply (ind_cases "G\<turnstile>S\<succ>T") |
|
625 by auto |
|
626 |
|
627 (*unused*) |
|
628 lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t" |
|
629 apply (ind_cases "G\<turnstile>S\<succ>T") |
|
630 by auto |
|
631 |
|
632 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> |
|
633 \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" |
|
634 apply (ind_cases "G\<turnstile>S\<succ>T") |
|
635 by auto |
|
636 |
|
637 |
|
638 section "casting relation" |
|
639 |
|
640 inductive "cast G" intros (* casting conversion, cf. 5.5 *) |
|
641 |
|
642 widen: "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" |
|
643 narrow: "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T" |
|
644 |
|
645 (* |
|
646 lemma ??unknown??: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>S\<succ>T\<rbrakk> \<Longrightarrow> R" |
|
647 deferred *) |
|
648 |
|
649 (*unused*) |
|
650 lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t" |
|
651 apply (ind_cases "G\<turnstile>S\<preceq>? T") |
|
652 by (auto dest: widen_RefT narrow_RefT) |
|
653 |
|
654 lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t" |
|
655 apply (ind_cases "G\<turnstile>S\<preceq>? T") |
|
656 by (auto dest: widen_RefT2 narrow_RefT2) |
|
657 |
|
658 (*unused*) |
|
659 lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t" |
|
660 apply (ind_cases "G\<turnstile>S\<preceq>? T") |
|
661 by (auto dest: widen_PrimT narrow_PrimT) |
|
662 |
|
663 lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt" |
|
664 apply (ind_cases "G\<turnstile>S\<preceq>? T") |
|
665 by (auto dest: widen_PrimT2 narrow_PrimT2) |
|
666 |
|
667 end |