10497
|
1 |
(* Title: HOL/BCV/JType.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
The type system of the JVM
|
|
7 |
*)
|
|
8 |
|
|
9 |
header "JVM Type System as Semilattice"
|
|
10 |
|
|
11 |
theory JType = WellForm + Err:
|
|
12 |
|
|
13 |
constdefs
|
|
14 |
is_ref :: "ty => bool"
|
|
15 |
"is_ref T == case T of PrimT t => False | RefT r => True"
|
|
16 |
|
|
17 |
sup :: "'c prog => ty => ty => ty err"
|
|
18 |
"sup G T1 T2 ==
|
|
19 |
case T1 of PrimT P1 => (case T2 of PrimT P2 => (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
|
|
20 |
| RefT R1 => (case T2 of PrimT P => Err | RefT R2 =>
|
|
21 |
(case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
|
|
22 |
| ClassT C => (case R2 of NullT => OK (Class C)
|
|
23 |
| ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
|
|
24 |
|
|
25 |
subtype :: "'c prog => ty => ty => bool"
|
|
26 |
"subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
|
|
27 |
|
|
28 |
is_ty :: "'c prog => ty => bool"
|
|
29 |
"is_ty G T == case T of PrimT P => True | RefT R =>
|
|
30 |
(case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
|
|
31 |
|
|
32 |
translations
|
|
33 |
"types G" == "Collect (is_type G)"
|
|
34 |
|
|
35 |
constdefs
|
|
36 |
esl :: "'c prog => ty esl"
|
|
37 |
"esl G == (types G, subtype G, sup G)"
|
|
38 |
|
|
39 |
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
|
|
40 |
by (auto elim: widen.elims)
|
|
41 |
|
|
42 |
lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
|
|
43 |
by (auto elim: widen.elims)
|
|
44 |
|
|
45 |
lemma is_tyI:
|
|
46 |
"[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
|
|
47 |
by (auto simp add: is_ty_def dest: subcls_C_Object
|
|
48 |
split: ty.splits ref_ty.splits)
|
|
49 |
|
|
50 |
lemma is_type_conv:
|
|
51 |
"wf_prog wf_mb G ==> is_type G T = is_ty G T"
|
|
52 |
proof
|
|
53 |
assume "is_type G T" "wf_prog wf_mb G"
|
|
54 |
thus "is_ty G T"
|
|
55 |
by (rule is_tyI)
|
|
56 |
next
|
|
57 |
assume wf: "wf_prog wf_mb G" and
|
|
58 |
ty: "is_ty G T"
|
|
59 |
|
|
60 |
show "is_type G T"
|
|
61 |
proof (cases T)
|
|
62 |
case PrimT
|
|
63 |
thus ?thesis by simp
|
|
64 |
next
|
|
65 |
fix R assume R: "T = RefT R"
|
|
66 |
with wf
|
|
67 |
have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
|
|
68 |
moreover
|
|
69 |
from R wf ty
|
|
70 |
have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
|
|
71 |
by (auto simp add: is_ty_def subcls1_def is_class_def class_def
|
|
72 |
elim: converse_rtranclE
|
|
73 |
split: ref_ty.splits)
|
|
74 |
ultimately
|
|
75 |
show ?thesis by blast
|
|
76 |
qed
|
|
77 |
qed
|
|
78 |
|
|
79 |
|
|
80 |
lemma order_widen:
|
|
81 |
"acyclic (subcls1 G) ==> order (subtype G)"
|
|
82 |
apply (unfold order_def lesub_def subtype_def)
|
|
83 |
apply (auto intro: widen_trans)
|
|
84 |
apply (case_tac x)
|
|
85 |
apply (case_tac y)
|
|
86 |
apply (auto simp add: PrimT_PrimT)
|
|
87 |
apply (case_tac y)
|
|
88 |
apply simp
|
|
89 |
apply simp
|
|
90 |
apply (case_tac ref_ty)
|
|
91 |
apply (case_tac ref_tya)
|
|
92 |
apply simp
|
|
93 |
apply simp
|
|
94 |
apply (case_tac ref_tya)
|
|
95 |
apply simp
|
|
96 |
apply simp
|
|
97 |
apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)
|
|
98 |
done
|
|
99 |
|
10592
|
100 |
lemma wf_converse_subcls1_impl_acc_subtype:
|
|
101 |
"wf ((subcls1 G)^-1) ==> acc (subtype G)"
|
|
102 |
apply (unfold acc_def lesssub_def)
|
|
103 |
apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
|
|
104 |
apply blast
|
|
105 |
apply (drule wf_trancl)
|
|
106 |
apply (simp add: wf_eq_minimal)
|
|
107 |
apply clarify
|
|
108 |
apply (unfold lesub_def subtype_def)
|
|
109 |
apply (rename_tac M T)
|
|
110 |
apply (case_tac "EX C. Class C : M")
|
|
111 |
prefer 2
|
|
112 |
apply (case_tac T)
|
|
113 |
apply (fastsimp simp add: PrimT_PrimT2)
|
|
114 |
apply simp
|
|
115 |
apply (subgoal_tac "ref_ty = NullT")
|
|
116 |
apply simp
|
|
117 |
apply (rule_tac x = NT in bexI)
|
|
118 |
apply (rule allI)
|
|
119 |
apply (rule impI, erule conjE)
|
|
120 |
apply (drule widen_RefT)
|
|
121 |
apply clarsimp
|
|
122 |
apply (case_tac t)
|
|
123 |
apply simp
|
|
124 |
apply simp
|
|
125 |
apply simp
|
|
126 |
apply (case_tac ref_ty)
|
|
127 |
apply simp
|
|
128 |
apply simp
|
|
129 |
apply (erule_tac x = "{C. Class C : M}" in allE)
|
|
130 |
apply auto
|
|
131 |
apply (rename_tac D)
|
|
132 |
apply (rule_tac x = "Class D" in bexI)
|
|
133 |
prefer 2
|
|
134 |
apply assumption
|
|
135 |
apply clarify
|
|
136 |
apply (frule widen_RefT)
|
|
137 |
apply (erule exE)
|
|
138 |
apply (case_tac t)
|
|
139 |
apply simp
|
|
140 |
apply simp
|
|
141 |
apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"])
|
|
142 |
apply simp
|
|
143 |
apply (erule rtranclE)
|
|
144 |
apply blast
|
|
145 |
apply (drule rtrancl_converseI)
|
|
146 |
apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)")
|
|
147 |
prefer 2
|
|
148 |
apply blast
|
|
149 |
apply simp
|
|
150 |
apply (blast intro: rtrancl_into_trancl2)
|
|
151 |
done
|
|
152 |
|
10497
|
153 |
lemma closed_err_types:
|
|
154 |
"[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |]
|
|
155 |
==> closed (err (types G)) (lift2 (sup G))"
|
|
156 |
apply (unfold closed_def plussub_def lift2_def sup_def)
|
|
157 |
apply (auto split: err.split)
|
|
158 |
apply (drule is_tyI, assumption)
|
|
159 |
apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps
|
|
160 |
split: ty.split ref_ty.split)
|
|
161 |
apply (blast dest!: is_lub_some_lub is_lubD is_ubD intro!: is_ubI)
|
|
162 |
done
|
|
163 |
|
|
164 |
|
|
165 |
lemma err_semilat_JType_esl_lemma:
|
|
166 |
"[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |]
|
|
167 |
==> err_semilat (esl G)"
|
|
168 |
proof -
|
|
169 |
assume wf_prog: "wf_prog wf_mb G"
|
|
170 |
assume univalent: "univalent (subcls1 G)"
|
|
171 |
assume acyclic: "acyclic (subcls1 G)"
|
|
172 |
|
|
173 |
hence "order (subtype G)"
|
|
174 |
by (rule order_widen)
|
|
175 |
moreover
|
|
176 |
from wf_prog univalent acyclic
|
|
177 |
have "closed (err (types G)) (lift2 (sup G))"
|
|
178 |
by (rule closed_err_types)
|
|
179 |
moreover
|
|
180 |
|
|
181 |
{ fix c1 c2
|
|
182 |
assume is_class: "is_class G c1" "is_class G c2"
|
|
183 |
with wf_prog
|
|
184 |
obtain
|
|
185 |
"G \<turnstile> c1 \<preceq>C Object"
|
|
186 |
"G \<turnstile> c2 \<preceq>C Object"
|
|
187 |
by (blast intro: subcls_C_Object)
|
|
188 |
with wf_prog univalent
|
|
189 |
obtain u where
|
|
190 |
"is_lub ((subcls1 G)^* ) c1 c2 u"
|
|
191 |
by (blast dest: univalent_has_lubs)
|
|
192 |
with acyclic
|
|
193 |
have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
|
|
194 |
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
|
|
195 |
} note this [intro]
|
|
196 |
|
|
197 |
{ fix t1 t2 s
|
|
198 |
assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"
|
|
199 |
hence "subtype G t1 s"
|
|
200 |
by (unfold sup_def subtype_def)
|
|
201 |
(cases s, auto intro: widen.null
|
|
202 |
split: ty.splits ref_ty.splits if_splits)
|
|
203 |
} note this [intro]
|
|
204 |
|
|
205 |
have
|
|
206 |
"\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y"
|
|
207 |
by (auto simp add: lesub_def plussub_def le_def lift2_def split: err.split)
|
|
208 |
moreover
|
|
209 |
|
|
210 |
{ fix c1 c2
|
|
211 |
assume "is_class G c1" "is_class G c2"
|
|
212 |
with wf_prog
|
|
213 |
obtain
|
|
214 |
"G \<turnstile> c1 \<preceq>C Object"
|
|
215 |
"G \<turnstile> c2 \<preceq>C Object"
|
|
216 |
by (blast intro: subcls_C_Object)
|
|
217 |
with wf_prog univalent
|
|
218 |
obtain u where
|
|
219 |
"is_lub ((subcls1 G)^* ) c2 c1 u"
|
|
220 |
by (blast dest: univalent_has_lubs)
|
|
221 |
with acyclic
|
|
222 |
have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c2 c1"
|
|
223 |
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
|
|
224 |
} note this [intro]
|
|
225 |
|
|
226 |
have "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G).
|
|
227 |
y <=_(le (subtype G)) x +_(lift2 (sup G)) y"
|
|
228 |
by (auto simp add: lesub_def plussub_def le_def sup_def subtype_def lift2_def
|
|
229 |
split: err.split ty.splits ref_ty.splits if_splits intro: widen.null)
|
|
230 |
moreover
|
|
231 |
|
|
232 |
have [intro]:
|
|
233 |
"!!a b c. [| G \<turnstile> a \<preceq> c; G \<turnstile> b \<preceq> c; sup G a b = Err |] ==> False"
|
|
234 |
by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def
|
|
235 |
split: ty.splits ref_ty.splits)
|
|
236 |
|
|
237 |
{ fix c1 c2 D
|
|
238 |
assume is_class: "is_class G c1" "is_class G c2"
|
|
239 |
assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
|
|
240 |
from wf_prog is_class
|
|
241 |
obtain
|
|
242 |
"G \<turnstile> c1 \<preceq>C Object"
|
|
243 |
"G \<turnstile> c2 \<preceq>C Object"
|
|
244 |
by (blast intro: subcls_C_Object)
|
|
245 |
with wf_prog univalent
|
|
246 |
obtain u where
|
|
247 |
lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
|
|
248 |
by (blast dest: univalent_has_lubs)
|
|
249 |
with acyclic
|
|
250 |
have "some_lub ((subcls1 G)^* ) c1 c2 = u"
|
|
251 |
by (rule some_lub_conv)
|
|
252 |
moreover
|
|
253 |
from lub le
|
|
254 |
have "G \<turnstile> u \<preceq>C D"
|
|
255 |
by (simp add: is_lub_def is_ub_def)
|
|
256 |
ultimately
|
|
257 |
have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
|
|
258 |
by blast
|
|
259 |
} note this [intro]
|
|
260 |
|
|
261 |
have [dest!]:
|
|
262 |
"!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
|
|
263 |
by (frule widen_Class, auto)
|
|
264 |
|
|
265 |
{ fix a b c d
|
|
266 |
assume "is_type G a" "is_type G b" "is_type G c" and
|
|
267 |
"G \<turnstile> a \<preceq> c" "G \<turnstile> b \<preceq> c" and
|
|
268 |
"sup G a b = OK d"
|
|
269 |
hence "G \<turnstile> d \<preceq> c"
|
|
270 |
by (auto simp add: sup_def split: ty.splits ref_ty.splits if_splits)
|
|
271 |
} note this [intro]
|
|
272 |
|
|
273 |
have
|
|
274 |
"\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G).
|
|
275 |
x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
|
|
276 |
by (simp add: lift2_def plussub_def lesub_def subtype_def le_def split: err.splits) blast
|
|
277 |
|
|
278 |
ultimately
|
|
279 |
|
|
280 |
show ?thesis
|
|
281 |
by (unfold esl_def semilat_def sl_def) auto
|
|
282 |
qed
|
|
283 |
|
|
284 |
lemma univalent_subcls1:
|
|
285 |
"wf_prog wf_mb G ==> univalent (subcls1 G)"
|
|
286 |
by (unfold wf_prog_def unique_def univalent_def subcls1_def) auto
|
|
287 |
|
|
288 |
ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *}
|
|
289 |
|
10592
|
290 |
theorem err_semilat_JType_esl:
|
|
291 |
"wf_prog wf_mb G ==> err_semilat (esl G)"
|
10497
|
292 |
by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma)
|
|
293 |
|
|
294 |
end
|