12951
|
1 |
(* Title: HOL/MicroJava/BV/BVExample.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Example Welltypings *}
|
|
7 |
|
|
8 |
theory BVExample = JVMListExample + Correct:
|
|
9 |
|
|
10 |
section "Setup"
|
|
11 |
text {*
|
|
12 |
Since the types @{typ cnam}, @{text vnam}, and @{text mname} are
|
|
13 |
anonymous, we describe distinctness of names in the example by axioms:
|
|
14 |
*}
|
|
15 |
axioms
|
|
16 |
distinct_classes: "list_nam \<noteq> test_nam"
|
|
17 |
distinct_fields: "val_nam \<noteq> next_nam"
|
|
18 |
|
|
19 |
text {* Shorthands for definitions we will have to use often in the
|
|
20 |
proofs below: *}
|
|
21 |
lemmas name_defs = list_name_def test_name_def val_name_def next_name_def
|
|
22 |
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def
|
|
23 |
OutOfMemoryC_def ClassCastC_def
|
|
24 |
lemmas class_defs = list_class_def test_class_def
|
|
25 |
|
|
26 |
text {* These auxiliary proofs are for efficiency: class lookup,
|
|
27 |
subclass relation, method and field lookup are computed only once:
|
|
28 |
*}
|
|
29 |
lemma class_Object [simp]:
|
|
30 |
"class E Object = Some (arbitrary, [],[])"
|
|
31 |
by (simp add: class_def system_defs E_def)
|
|
32 |
|
|
33 |
lemma class_NullPointer [simp]:
|
|
34 |
"class E (Xcpt NullPointer) = Some (Object, [], [])"
|
|
35 |
by (simp add: class_def system_defs E_def)
|
|
36 |
|
|
37 |
lemma class_OutOfMemory [simp]:
|
|
38 |
"class E (Xcpt OutOfMemory) = Some (Object, [], [])"
|
|
39 |
by (simp add: class_def system_defs E_def)
|
|
40 |
|
|
41 |
lemma class_ClassCast [simp]:
|
|
42 |
"class E (Xcpt ClassCast) = Some (Object, [], [])"
|
|
43 |
by (simp add: class_def system_defs E_def)
|
|
44 |
|
|
45 |
lemma class_list [simp]:
|
|
46 |
"class E list_name = Some list_class"
|
|
47 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
|
|
48 |
|
|
49 |
lemma class_test [simp]:
|
|
50 |
"class E test_name = Some test_class"
|
|
51 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
|
|
52 |
|
|
53 |
lemma E_classes [simp]:
|
|
54 |
"{C. is_class E C} = {list_name, test_name, Xcpt NullPointer,
|
|
55 |
Xcpt ClassCast, Xcpt OutOfMemory, Object}"
|
|
56 |
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
|
|
57 |
|
|
58 |
text {* The subclass releation spelled out: *}
|
|
59 |
lemma subcls1:
|
|
60 |
"subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
|
|
61 |
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
|
|
62 |
apply (simp add: subcls1_def2)
|
|
63 |
apply (simp add: name_defs class_defs system_defs E_def class_def)
|
|
64 |
apply (auto split: split_if_asm)
|
|
65 |
done
|
|
66 |
|
|
67 |
text {* The subclass relation is acyclic; hence its converse is well founded: *}
|
|
68 |
lemma notin_rtrancl:
|
|
69 |
"(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
|
|
70 |
by (auto elim: converse_rtranclE)
|
|
71 |
|
|
72 |
lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
|
|
73 |
apply (rule acyclicI)
|
|
74 |
apply (simp add: subcls1)
|
|
75 |
apply (auto dest!: tranclD)
|
|
76 |
apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
|
|
77 |
done
|
|
78 |
|
|
79 |
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
|
|
80 |
apply (rule finite_acyclic_wf_converse)
|
|
81 |
apply (simp add: subcls1)
|
|
82 |
apply (rule acyclic_subcls1_E)
|
|
83 |
done
|
|
84 |
|
|
85 |
text {* Method and field lookup: *}
|
|
86 |
lemma method_Object [simp]:
|
|
87 |
"method (E, Object) = empty"
|
|
88 |
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
|
|
89 |
|
|
90 |
lemma method_append [simp]:
|
|
91 |
"method (E, list_name) (append_name, [Class list_name]) =
|
|
92 |
Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
|
|
93 |
apply (insert class_list)
|
|
94 |
apply (unfold list_class_def)
|
|
95 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E])
|
|
96 |
apply simp
|
|
97 |
done
|
|
98 |
|
|
99 |
lemma method_makelist [simp]:
|
|
100 |
"method (E, test_name) (makelist_name, []) =
|
|
101 |
Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
|
|
102 |
apply (insert class_test)
|
|
103 |
apply (unfold test_class_def)
|
|
104 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E])
|
|
105 |
apply simp
|
|
106 |
done
|
|
107 |
|
|
108 |
lemma field_val [simp]:
|
|
109 |
"field (E, list_name) val_name = Some (list_name, PrimT Integer)"
|
|
110 |
apply (unfold field_def)
|
|
111 |
apply (insert class_list)
|
|
112 |
apply (unfold list_class_def)
|
|
113 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
|
|
114 |
apply simp
|
|
115 |
done
|
|
116 |
|
|
117 |
lemma field_next [simp]:
|
|
118 |
"field (E, list_name) next_name = Some (list_name, Class list_name)"
|
|
119 |
apply (unfold field_def)
|
|
120 |
apply (insert class_list)
|
|
121 |
apply (unfold list_class_def)
|
|
122 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
|
|
123 |
apply (simp add: name_defs distinct_fields [symmetric])
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma [simp]: "fields (E, Object) = []"
|
|
127 |
by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
|
|
128 |
|
|
129 |
lemma [simp]: "fields (E, Xcpt NullPointer) = []"
|
|
130 |
by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
|
|
131 |
|
|
132 |
lemma [simp]: "fields (E, Xcpt ClassCast) = []"
|
|
133 |
by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
|
|
134 |
|
|
135 |
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
|
|
136 |
by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
|
|
137 |
|
|
138 |
lemma [simp]: "fields (E, test_name) = []"
|
|
139 |
apply (insert class_test)
|
|
140 |
apply (unfold test_class_def)
|
|
141 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
|
|
142 |
apply simp
|
|
143 |
done
|
|
144 |
|
|
145 |
lemmas [simp] = is_class_def
|
|
146 |
|
|
147 |
text {*
|
|
148 |
The next definition and three proof rules implement an algorithm to
|
|
149 |
enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"}
|
|
150 |
transforms a goal of the form
|
|
151 |
@{prop [display] "pc < n \<Longrightarrow> P pc"}
|
|
152 |
into a series of goals
|
|
153 |
@{prop [display] "P 0"}
|
|
154 |
@{prop [display] "P (Suc 0)"}
|
|
155 |
|
|
156 |
@{text "\<dots>"}
|
|
157 |
|
|
158 |
@{prop [display] "P n"}
|
|
159 |
*}
|
|
160 |
constdefs
|
|
161 |
intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
|
|
162 |
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
|
|
163 |
|
|
164 |
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
|
|
165 |
by (simp add: intervall_def)
|
|
166 |
|
|
167 |
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
|
|
168 |
apply (cases "x=n0")
|
|
169 |
apply (auto simp add: intervall_def)
|
|
170 |
apply arith
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x"
|
|
174 |
by (unfold intervall_def) arith
|
|
175 |
|
|
176 |
|
|
177 |
section "Program structure"
|
|
178 |
|
|
179 |
text {*
|
|
180 |
The program is structurally wellformed:
|
|
181 |
*}
|
|
182 |
lemma wf_struct:
|
|
183 |
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
|
|
184 |
proof -
|
|
185 |
have "unique E"
|
|
186 |
by (simp add: system_defs E_def class_defs name_defs distinct_classes)
|
|
187 |
moreover
|
|
188 |
have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
|
|
189 |
hence "wf_syscls E" by (rule wf_syscls)
|
|
190 |
moreover
|
|
191 |
have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
|
|
192 |
moreover
|
|
193 |
have "wf_cdecl ?mb E NullPointerC"
|
|
194 |
by (auto elim: notin_rtrancl
|
|
195 |
simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
|
|
196 |
moreover
|
|
197 |
have "wf_cdecl ?mb E ClassCastC"
|
|
198 |
by (auto elim: notin_rtrancl
|
|
199 |
simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
|
|
200 |
moreover
|
|
201 |
have "wf_cdecl ?mb E OutOfMemoryC"
|
|
202 |
by (auto elim: notin_rtrancl
|
|
203 |
simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
|
|
204 |
moreover
|
|
205 |
have "wf_cdecl ?mb E (list_name, list_class)"
|
|
206 |
apply (auto elim!: notin_rtrancl
|
|
207 |
simp add: wf_cdecl_def wf_fdecl_def list_class_def
|
|
208 |
wf_mdecl_def wf_mhead_def subcls1)
|
|
209 |
apply (auto simp add: name_defs distinct_classes distinct_fields)
|
|
210 |
done
|
|
211 |
moreover
|
|
212 |
have "wf_cdecl ?mb E (test_name, test_class)"
|
|
213 |
apply (auto elim!: notin_rtrancl
|
|
214 |
simp add: wf_cdecl_def wf_fdecl_def test_class_def
|
|
215 |
wf_mdecl_def wf_mhead_def subcls1)
|
|
216 |
apply (auto simp add: name_defs distinct_classes distinct_fields)
|
|
217 |
done
|
|
218 |
ultimately
|
|
219 |
show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
|
|
220 |
qed
|
|
221 |
|
|
222 |
section "Welltypings"
|
|
223 |
text {*
|
|
224 |
We show welltypings of the methods @{term append_name} in class @{term list_name},
|
|
225 |
and @{term makelist_name} in class @{term test_name}:
|
|
226 |
*}
|
|
227 |
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
|
|
228 |
declare appInvoke [simp del]
|
|
229 |
|
|
230 |
constdefs
|
|
231 |
phi_append :: method_type ("\<phi>\<^sub>a")
|
|
232 |
"\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [
|
|
233 |
( [], [Class list_name, Class list_name]),
|
|
234 |
( [Class list_name], [Class list_name, Class list_name]),
|
|
235 |
( [Class list_name], [Class list_name, Class list_name]),
|
|
236 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
|
|
237 |
([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
|
|
238 |
( [Class list_name], [Class list_name, Class list_name]),
|
|
239 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
|
|
240 |
( [PrimT Void], [Class list_name, Class list_name]),
|
|
241 |
( [Class Object], [Class list_name, Class list_name]),
|
|
242 |
( [], [Class list_name, Class list_name]),
|
|
243 |
( [Class list_name], [Class list_name, Class list_name]),
|
|
244 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]),
|
|
245 |
( [], [Class list_name, Class list_name]),
|
|
246 |
( [PrimT Void], [Class list_name, Class list_name])]"
|
|
247 |
|
|
248 |
lemma wt_append [simp]:
|
|
249 |
"wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
|
|
250 |
[(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
|
|
251 |
apply (simp add: wt_method_def append_ins_def phi_append_def
|
|
252 |
wt_start_def wt_instr_def)
|
|
253 |
apply clarify
|
|
254 |
apply (elim pc_end pc_next pc_0)
|
|
255 |
apply simp
|
|
256 |
apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
|
|
257 |
apply simp
|
|
258 |
apply simp
|
|
259 |
apply (fastsimp simp add: sup_state_conv subcls1)
|
|
260 |
apply simp
|
|
261 |
apply (simp add: app_def xcpt_app_def)
|
|
262 |
apply simp
|
|
263 |
apply simp
|
|
264 |
apply simp
|
|
265 |
apply (simp add: match_exception_entry_def)
|
|
266 |
apply (simp add: match_exception_entry_def)
|
|
267 |
apply simp
|
|
268 |
apply simp
|
|
269 |
done
|
|
270 |
|
|
271 |
text {* Some shorthands to make the welltyping of method @{term
|
|
272 |
makelist_name} easier to read *}
|
|
273 |
syntax
|
|
274 |
list :: ty
|
|
275 |
test :: ty
|
|
276 |
translations
|
|
277 |
"list" == "Class list_name"
|
|
278 |
"test" == "Class test_name"
|
|
279 |
|
|
280 |
constdefs
|
|
281 |
phi_makelist :: method_type ("\<phi>\<^sub>m")
|
|
282 |
"\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [
|
|
283 |
( [], [OK test, Err , Err ]),
|
|
284 |
( [list], [OK test, Err , Err ]),
|
|
285 |
( [list, list], [OK test, Err , Err ]),
|
|
286 |
( [list], [OK list, Err , Err ]),
|
|
287 |
( [PrimT Integer, list], [OK list, Err , Err ]),
|
|
288 |
( [], [OK list, Err , Err ]),
|
|
289 |
( [list], [OK list, Err , Err ]),
|
|
290 |
( [list, list], [OK list, Err , Err ]),
|
|
291 |
( [list], [OK list, OK list, Err ]),
|
|
292 |
( [PrimT Integer, list], [OK list, OK list, Err ]),
|
|
293 |
( [], [OK list, OK list, Err ]),
|
|
294 |
( [list], [OK list, OK list, Err ]),
|
|
295 |
( [list, list], [OK list, OK list, Err ]),
|
|
296 |
( [list], [OK list, OK list, OK list]),
|
|
297 |
( [PrimT Integer, list], [OK list, OK list, OK list]),
|
|
298 |
( [], [OK list, OK list, OK list]),
|
|
299 |
( [list], [OK list, OK list, OK list]),
|
|
300 |
( [list, list], [OK list, OK list, OK list]),
|
|
301 |
( [PrimT Void], [OK list, OK list, OK list]),
|
|
302 |
( [list, PrimT Void], [OK list, OK list, OK list]),
|
|
303 |
( [list, list, PrimT Void], [OK list, OK list, OK list]),
|
|
304 |
( [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
|
|
305 |
( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
|
|
306 |
|
|
307 |
lemma wt_makelist [simp]:
|
|
308 |
"wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
|
|
309 |
apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
|
|
310 |
apply (simp add: wt_start_def nat_number_of)
|
|
311 |
apply (simp add: wt_instr_def)
|
|
312 |
apply clarify
|
|
313 |
apply (elim pc_end pc_next pc_0)
|
|
314 |
apply (simp add: match_exception_entry_def)
|
|
315 |
apply simp
|
|
316 |
apply simp
|
|
317 |
apply simp
|
|
318 |
apply (simp add: match_exception_entry_def)
|
|
319 |
apply (simp add: match_exception_entry_def)
|
|
320 |
apply simp
|
|
321 |
apply simp
|
|
322 |
apply simp
|
|
323 |
apply (simp add: match_exception_entry_def)
|
|
324 |
apply (simp add: match_exception_entry_def)
|
|
325 |
apply simp
|
|
326 |
apply simp
|
|
327 |
apply simp
|
|
328 |
apply (simp add: match_exception_entry_def)
|
|
329 |
apply (simp add: match_exception_entry_def)
|
|
330 |
apply simp
|
|
331 |
apply (simp add: app_def xcpt_app_def)
|
|
332 |
apply simp
|
|
333 |
apply simp
|
|
334 |
apply (simp add: app_def xcpt_app_def)
|
|
335 |
apply simp
|
|
336 |
apply simp
|
|
337 |
done
|
|
338 |
|
|
339 |
text {* The whole program is welltyped: *}
|
|
340 |
constdefs
|
|
341 |
Phi :: prog_type ("\<Phi>")
|
|
342 |
"\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
|
|
343 |
if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
|
|
344 |
|
|
345 |
lemma wf_prog:
|
|
346 |
"wt_jvm_prog E \<Phi>"
|
|
347 |
apply (unfold wt_jvm_prog_def)
|
|
348 |
apply (rule wf_mb'E [OF wf_struct])
|
|
349 |
apply (simp add: E_def)
|
|
350 |
apply clarify
|
|
351 |
apply (fold E_def)
|
|
352 |
apply (simp add: system_defs class_defs Phi_def)
|
|
353 |
apply auto
|
|
354 |
done
|
|
355 |
|
|
356 |
|
|
357 |
section "Conformance"
|
|
358 |
text {* Execution of the program will be typesafe, because its
|
|
359 |
start state conforms to the welltyping: *}
|
|
360 |
|
|
361 |
lemma [simp]: "preallocated start_heap"
|
|
362 |
apply (unfold start_heap_def preallocated_def)
|
|
363 |
apply auto
|
|
364 |
apply (case_tac x)
|
|
365 |
apply auto
|
|
366 |
done
|
|
367 |
|
|
368 |
lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
|
|
369 |
apply (simp add: correct_state_def start_state_def test_class_def)
|
|
370 |
apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
|
|
371 |
apply (simp add: Phi_def phi_makelist_def)
|
|
372 |
apply (simp add: correct_frame_def)
|
|
373 |
apply (simp add: make_list_ins_def)
|
|
374 |
apply (simp add: conf_def start_heap_def)
|
|
375 |
done
|
|
376 |
|
|
377 |
end |