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