author | haftmann |
Mon, 26 Dec 2011 18:32:43 +0100 | |
changeset 45986 | c9e50153e5ae |
parent 45985 | 2d399a776de2 |
child 45990 | b7b905b23b2a |
permissions | -rw-r--r-- |
12951 | 1 |
(* Title: HOL/MicroJava/BV/BVExample.thy |
2 |
Author: Gerwin Klein |
|
3 |
*) |
|
4 |
||
12972 | 5 |
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} |
12951 | 6 |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
7 |
theory BVExample |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40077
diff
changeset
|
8 |
imports |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40077
diff
changeset
|
9 |
"../JVM/JVMListExample" |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40077
diff
changeset
|
10 |
BVSpecTypeSafe |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40077
diff
changeset
|
11 |
JVM |
45985 | 12 |
"~~/src/HOL/Library/More_Set" |
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
13 |
begin |
12951 | 14 |
|
12972 | 15 |
text {* |
16 |
This theory shows type correctness of the example program in section |
|
17 |
\ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
|
18 |
explicitly providing a welltyping. It also shows that the start |
|
19 |
state of the program conforms to the welltyping; hence type safe |
|
20 |
execution is guaranteed. |
|
21 |
*} |
|
22 |
||
12951 | 23 |
section "Setup" |
24 |
||
13101 | 25 |
text {* Abbreviations for definitions we will have to use often in the |
12951 | 26 |
proofs below: *} |
13101 | 27 |
lemmas name_defs = list_name_def test_name_def val_name_def next_name_def |
12951 | 28 |
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def |
29 |
OutOfMemoryC_def ClassCastC_def |
|
30 |
lemmas class_defs = list_class_def test_class_def |
|
31 |
||
32 |
text {* These auxiliary proofs are for efficiency: class lookup, |
|
33 |
subclass relation, method and field lookup are computed only once: |
|
34 |
*} |
|
35 |
lemma class_Object [simp]: |
|
28520 | 36 |
"class E Object = Some (undefined, [],[])" |
12951 | 37 |
by (simp add: class_def system_defs E_def) |
38 |
||
39 |
lemma class_NullPointer [simp]: |
|
40 |
"class E (Xcpt NullPointer) = Some (Object, [], [])" |
|
41 |
by (simp add: class_def system_defs E_def) |
|
42 |
||
43 |
lemma class_OutOfMemory [simp]: |
|
44 |
"class E (Xcpt OutOfMemory) = Some (Object, [], [])" |
|
45 |
by (simp add: class_def system_defs E_def) |
|
46 |
||
47 |
lemma class_ClassCast [simp]: |
|
48 |
"class E (Xcpt ClassCast) = Some (Object, [], [])" |
|
49 |
by (simp add: class_def system_defs E_def) |
|
50 |
||
51 |
lemma class_list [simp]: |
|
52 |
"class E list_name = Some list_class" |
|
53 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric]) |
|
54 |
||
55 |
lemma class_test [simp]: |
|
56 |
"class E test_name = Some test_class" |
|
57 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric]) |
|
58 |
||
59 |
lemma E_classes [simp]: |
|
60 |
"{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, |
|
61 |
Xcpt ClassCast, Xcpt OutOfMemory, Object}" |
|
62 |
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs) |
|
63 |
||
64 |
text {* The subclass releation spelled out: *} |
|
65 |
lemma subcls1: |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
66 |
"subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
67 |
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}" |
31197
c1c163ec6c44
fine-tuned elimination of comprehensions involving x=t.
nipkow
parents:
31168
diff
changeset
|
68 |
apply (simp add: subcls1_def2) |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28520
diff
changeset
|
69 |
apply (simp add: name_defs class_defs system_defs E_def class_def) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
70 |
apply (simp add: Sigma_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
71 |
apply auto |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28520
diff
changeset
|
72 |
done |
12951 | 73 |
|
74 |
text {* The subclass relation is acyclic; hence its converse is well founded: *} |
|
75 |
lemma notin_rtrancl: |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
76 |
"(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
77 |
by (auto elim: converse_rtranclE) |
12951 | 78 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
79 |
lemma acyclic_subcls1_E: "acyclic (subcls1 E)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
80 |
apply (rule acyclicI) |
12951 | 81 |
apply (simp add: subcls1) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
82 |
apply (auto dest!: tranclD) |
12951 | 83 |
apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes) |
84 |
done |
|
85 |
||
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
86 |
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
87 |
apply (rule finite_acyclic_wf_converse) |
23757 | 88 |
apply (simp add: subcls1 del: insert_iff) |
12951 | 89 |
apply (rule acyclic_subcls1_E) |
90 |
done |
|
91 |
||
92 |
text {* Method and field lookup: *} |
|
93 |
lemma method_Object [simp]: |
|
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31197
diff
changeset
|
94 |
"method (E, Object) = Map.empty" |
12951 | 95 |
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E]) |
96 |
||
97 |
lemma method_append [simp]: |
|
98 |
"method (E, list_name) (append_name, [Class list_name]) = |
|
99 |
Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])" |
|
100 |
apply (insert class_list) |
|
101 |
apply (unfold list_class_def) |
|
102 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E]) |
|
103 |
apply simp |
|
104 |
done |
|
105 |
||
106 |
lemma method_makelist [simp]: |
|
107 |
"method (E, test_name) (makelist_name, []) = |
|
108 |
Some (test_name, PrimT Void, 3, 2, make_list_ins, [])" |
|
109 |
apply (insert class_test) |
|
110 |
apply (unfold test_class_def) |
|
111 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E]) |
|
112 |
apply simp |
|
113 |
done |
|
114 |
||
115 |
lemma field_val [simp]: |
|
116 |
"field (E, list_name) val_name = Some (list_name, PrimT Integer)" |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
117 |
apply (unfold TypeRel.field_def) |
12951 | 118 |
apply (insert class_list) |
119 |
apply (unfold list_class_def) |
|
120 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
121 |
apply simp |
|
122 |
done |
|
123 |
||
124 |
lemma field_next [simp]: |
|
125 |
"field (E, list_name) next_name = Some (list_name, Class list_name)" |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
126 |
apply (unfold TypeRel.field_def) |
12951 | 127 |
apply (insert class_list) |
128 |
apply (unfold list_class_def) |
|
129 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
130 |
apply (simp add: name_defs distinct_fields [symmetric]) |
|
131 |
done |
|
132 |
||
133 |
lemma [simp]: "fields (E, Object) = []" |
|
134 |
by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E]) |
|
135 |
||
136 |
lemma [simp]: "fields (E, Xcpt NullPointer) = []" |
|
137 |
by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E]) |
|
138 |
||
139 |
lemma [simp]: "fields (E, Xcpt ClassCast) = []" |
|
140 |
by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E]) |
|
141 |
||
142 |
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []" |
|
143 |
by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E]) |
|
144 |
||
145 |
lemma [simp]: "fields (E, test_name) = []" |
|
146 |
apply (insert class_test) |
|
147 |
apply (unfold test_class_def) |
|
148 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
149 |
apply simp |
|
150 |
done |
|
151 |
||
152 |
lemmas [simp] = is_class_def |
|
153 |
||
154 |
text {* |
|
155 |
The next definition and three proof rules implement an algorithm to |
|
156 |
enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} |
|
157 |
transforms a goal of the form |
|
158 |
@{prop [display] "pc < n \<Longrightarrow> P pc"} |
|
159 |
into a series of goals |
|
160 |
@{prop [display] "P 0"} |
|
161 |
@{prop [display] "P (Suc 0)"} |
|
162 |
||
163 |
@{text "\<dots>"} |
|
164 |
||
165 |
@{prop [display] "P n"} |
|
166 |
*} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
167 |
definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where |
12951 | 168 |
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b" |
169 |
||
170 |
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x" |
|
171 |
by (simp add: intervall_def) |
|
172 |
||
173 |
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x" |
|
174 |
apply (cases "x=n0") |
|
13187 | 175 |
apply (auto simp add: intervall_def) |
12951 | 176 |
done |
177 |
||
178 |
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" |
|
179 |
by (unfold intervall_def) arith |
|
180 |
||
181 |
||
182 |
section "Program structure" |
|
183 |
||
184 |
text {* |
|
185 |
The program is structurally wellformed: |
|
186 |
*} |
|
14045 | 187 |
|
12951 | 188 |
lemma wf_struct: |
189 |
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E") |
|
190 |
proof - |
|
191 |
have "unique E" |
|
192 |
by (simp add: system_defs E_def class_defs name_defs distinct_classes) |
|
193 |
moreover |
|
194 |
have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def) |
|
195 |
hence "wf_syscls E" by (rule wf_syscls) |
|
196 |
moreover |
|
197 |
have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def) |
|
198 |
moreover |
|
199 |
have "wf_cdecl ?mb E NullPointerC" |
|
200 |
by (auto elim: notin_rtrancl |
|
201 |
simp add: wf_cdecl_def name_defs NullPointerC_def subcls1) |
|
202 |
moreover |
|
203 |
have "wf_cdecl ?mb E ClassCastC" |
|
204 |
by (auto elim: notin_rtrancl |
|
205 |
simp add: wf_cdecl_def name_defs ClassCastC_def subcls1) |
|
206 |
moreover |
|
207 |
have "wf_cdecl ?mb E OutOfMemoryC" |
|
208 |
by (auto elim: notin_rtrancl |
|
209 |
simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1) |
|
210 |
moreover |
|
211 |
have "wf_cdecl ?mb E (list_name, list_class)" |
|
212 |
apply (auto elim!: notin_rtrancl |
|
213 |
simp add: wf_cdecl_def wf_fdecl_def list_class_def |
|
214 |
wf_mdecl_def wf_mhead_def subcls1) |
|
215 |
apply (auto simp add: name_defs distinct_classes distinct_fields) |
|
216 |
done |
|
217 |
moreover |
|
218 |
have "wf_cdecl ?mb E (test_name, test_class)" |
|
219 |
apply (auto elim!: notin_rtrancl |
|
220 |
simp add: wf_cdecl_def wf_fdecl_def test_class_def |
|
221 |
wf_mdecl_def wf_mhead_def subcls1) |
|
222 |
apply (auto simp add: name_defs distinct_classes distinct_fields) |
|
223 |
done |
|
224 |
ultimately |
|
14045 | 225 |
show ?thesis |
226 |
by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def) |
|
12951 | 227 |
qed |
228 |
||
229 |
section "Welltypings" |
|
230 |
text {* |
|
231 |
We show welltypings of the methods @{term append_name} in class @{term list_name}, |
|
232 |
and @{term makelist_name} in class @{term test_name}: |
|
233 |
*} |
|
234 |
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def |
|
235 |
declare appInvoke [simp del] |
|
236 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
237 |
definition phi_append :: method_type ("\<phi>\<^sub>a") where |
12951 | 238 |
"\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ |
239 |
( [], [Class list_name, Class list_name]), |
|
240 |
( [Class list_name], [Class list_name, Class list_name]), |
|
241 |
( [Class list_name], [Class list_name, Class list_name]), |
|
242 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
243 |
([NT, Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
244 |
( [Class list_name], [Class list_name, Class list_name]), |
|
245 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
246 |
( [PrimT Void], [Class list_name, Class list_name]), |
|
247 |
( [Class Object], [Class list_name, Class list_name]), |
|
248 |
( [], [Class list_name, Class list_name]), |
|
249 |
( [Class list_name], [Class list_name, Class list_name]), |
|
250 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
251 |
( [], [Class list_name, Class list_name]), |
|
252 |
( [PrimT Void], [Class list_name, Class list_name])]" |
|
253 |
||
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
254 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
255 |
lemma bounded_append [simp]: |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
256 |
"check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
257 |
apply (simp add: check_bounded_def) |
40077 | 258 |
apply (simp add: eval_nat_numeral append_ins_def) |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
259 |
apply (rule allI, rule impI) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
260 |
apply (elim pc_end pc_next pc_0) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
261 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
262 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
263 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
264 |
lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
265 |
apply (auto simp add: check_types_def phi_append_def JVM_states_unfold) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
266 |
apply (unfold list_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
267 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
268 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
269 |
|
12951 | 270 |
lemma wt_append [simp]: |
271 |
"wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins |
|
272 |
[(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
273 |
apply (simp add: wt_method_def wt_start_def wt_instr_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
274 |
apply (simp add: phi_append_def append_ins_def) |
12951 | 275 |
apply clarify |
276 |
apply (elim pc_end pc_next pc_0) |
|
277 |
apply simp |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44035
diff
changeset
|
278 |
apply (fastforce simp add: match_exception_entry_def sup_state_conv subcls1) |
12951 | 279 |
apply simp |
280 |
apply simp |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44035
diff
changeset
|
281 |
apply (fastforce simp add: sup_state_conv subcls1) |
12951 | 282 |
apply simp |
283 |
apply (simp add: app_def xcpt_app_def) |
|
284 |
apply simp |
|
285 |
apply simp |
|
286 |
apply simp |
|
287 |
apply (simp add: match_exception_entry_def) |
|
288 |
apply (simp add: match_exception_entry_def) |
|
289 |
apply simp |
|
290 |
apply simp |
|
291 |
done |
|
292 |
||
13006 | 293 |
text {* Some abbreviations for readability *} |
35102 | 294 |
abbreviation Clist :: ty |
295 |
where "Clist == Class list_name" |
|
296 |
abbreviation Ctest :: ty |
|
297 |
where "Ctest == Class test_name" |
|
12951 | 298 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
299 |
definition phi_makelist :: method_type ("\<phi>\<^sub>m") where |
12951 | 300 |
"\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
301 |
( [], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
302 |
( [Clist], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
303 |
( [Clist, Clist], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
304 |
( [Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
305 |
( [PrimT Integer, Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
306 |
( [], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
307 |
( [Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
308 |
( [Clist, Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
309 |
( [Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
310 |
( [PrimT Integer, Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
311 |
( [], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
312 |
( [Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
313 |
( [Clist, Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
314 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
315 |
( [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
316 |
( [], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
317 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
318 |
( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
319 |
( [PrimT Void], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
320 |
( [], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
321 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
322 |
( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
323 |
( [PrimT Void], [OK Clist, OK Clist, OK Clist])]" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
324 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
325 |
lemma bounded_makelist [simp]: "check_bounded make_list_ins []" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
326 |
apply (simp add: check_bounded_def) |
40077 | 327 |
apply (simp add: eval_nat_numeral make_list_ins_def) |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
328 |
apply (rule allI, rule impI) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
329 |
apply (elim pc_end pc_next pc_0) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
330 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
331 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
332 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
333 |
lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
334 |
apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
335 |
apply (unfold list_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
336 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
337 |
done |
12951 | 338 |
|
339 |
lemma wt_makelist [simp]: |
|
340 |
"wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
341 |
apply (simp add: wt_method_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
342 |
apply (simp add: make_list_ins_def phi_makelist_def) |
40077 | 343 |
apply (simp add: wt_start_def eval_nat_numeral) |
12951 | 344 |
apply (simp add: wt_instr_def) |
345 |
apply clarify |
|
346 |
apply (elim pc_end pc_next pc_0) |
|
347 |
apply (simp add: match_exception_entry_def) |
|
348 |
apply simp |
|
349 |
apply simp |
|
350 |
apply simp |
|
351 |
apply (simp add: match_exception_entry_def) |
|
352 |
apply (simp add: match_exception_entry_def) |
|
353 |
apply simp |
|
354 |
apply simp |
|
355 |
apply simp |
|
356 |
apply (simp add: match_exception_entry_def) |
|
357 |
apply (simp add: match_exception_entry_def) |
|
358 |
apply simp |
|
359 |
apply simp |
|
360 |
apply simp |
|
361 |
apply (simp add: match_exception_entry_def) |
|
362 |
apply (simp add: match_exception_entry_def) |
|
363 |
apply simp |
|
364 |
apply (simp add: app_def xcpt_app_def) |
|
13101 | 365 |
apply simp |
12951 | 366 |
apply simp |
367 |
apply simp |
|
13101 | 368 |
apply (simp add: app_def xcpt_app_def) |
12951 | 369 |
apply simp |
370 |
done |
|
371 |
||
372 |
text {* The whole program is welltyped: *} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
373 |
definition Phi :: prog_type ("\<Phi>") where |
13101 | 374 |
"\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else |
375 |
if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []" |
|
13139 | 376 |
|
12951 | 377 |
lemma wf_prog: |
13101 | 378 |
"wt_jvm_prog E \<Phi>" |
12951 | 379 |
apply (unfold wt_jvm_prog_def) |
380 |
apply (rule wf_mb'E [OF wf_struct]) |
|
381 |
apply (simp add: E_def) |
|
382 |
apply clarify |
|
383 |
apply (fold E_def) |
|
13101 | 384 |
apply (simp add: system_defs class_defs Phi_def) |
12951 | 385 |
apply auto |
13101 | 386 |
done |
12951 | 387 |
|
388 |
||
389 |
section "Conformance" |
|
390 |
text {* Execution of the program will be typesafe, because its |
|
391 |
start state conforms to the welltyping: *} |
|
392 |
||
13052 | 393 |
lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>" |
394 |
apply (rule BV_correct_initial) |
|
395 |
apply (rule wf_prog) |
|
396 |
apply simp |
|
397 |
apply simp |
|
12951 | 398 |
done |
399 |
||
13092 | 400 |
|
401 |
section "Example for code generation: inferring method types" |
|
402 |
||
28520 | 403 |
definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
404 |
exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where |
|
405 |
"test_kil G C pTs rT mxs mxl et instr = |
|
13092 | 406 |
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
407 |
start = OK first#(replicate (size instr - 1) (OK None)) |
|
408 |
in kiljvm G mxs (1+size pTs+mxl) rT et instr start)" |
|
409 |
||
410 |
lemma [code]: |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
411 |
"unstables r step ss = |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
412 |
foldr (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
413 |
proof - |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
414 |
have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
415 |
apply (unfold unstables_def) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
416 |
apply (rule equalityI) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
417 |
apply (rule subsetI) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
418 |
apply (erule CollectE) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
419 |
apply (erule conjE) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
420 |
apply (rule UN_I) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
421 |
apply simp |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
422 |
apply simp |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
423 |
apply (rule subsetI) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
424 |
apply (erule UN_E) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
425 |
apply (case_tac "\<not> stable r step ss p") |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
426 |
apply simp+ |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
427 |
done |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
428 |
also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
429 |
also note Sup_set_foldr also note foldr_map |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
430 |
also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) = |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
431 |
(\<lambda>p A. if \<not>stable r step ss p then insert p A else A)" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
432 |
by(auto simp add: fun_eq_iff) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
433 |
finally show ?thesis . |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
434 |
qed |
13092 | 435 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
436 |
definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]: |
28520 | 437 |
"some_elem = (%S. SOME x. x : S)" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
438 |
code_const some_elem |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
439 |
(SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)") |
13092 | 440 |
|
28520 | 441 |
text {* This code setup is just a demonstration and \emph{not} sound! *} |
442 |
||
443 |
lemma False |
|
444 |
proof - |
|
445 |
have "some_elem (set [False, True]) = False" |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
446 |
by eval |
28520 | 447 |
moreover have "some_elem (set [True, False]) = True" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
448 |
by eval |
28520 | 449 |
ultimately show False |
450 |
by (simp add: some_elem_def) |
|
451 |
qed |
|
452 |
||
453 |
lemma [code]: |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45985
diff
changeset
|
454 |
"iter f step ss w = while (\<lambda>(ss, w). \<not> Set.is_empty w) |
28520 | 455 |
(\<lambda>(ss, w). |
456 |
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) |
|
457 |
(ss, w)" |
|
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45985
diff
changeset
|
458 |
unfolding iter_def Set.is_empty_def some_elem_def .. |
20593 | 459 |
|
13092 | 460 |
lemma JVM_sup_unfold [code]: |
461 |
"JVMType.sup S m n = lift2 (Opt.sup |
|
462 |
(Product.sup (Listn.sup (JType.sup S)) |
|
463 |
(\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |
|
464 |
apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def |
|
465 |
stk_esl_def reg_sl_def Product.esl_def |
|
466 |
Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) |
|
467 |
by simp |
|
468 |
||
28520 | 469 |
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
470 |
lemmas [code] = lesub_def plussub_def |
13092 | 471 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44890
diff
changeset
|
472 |
lemmas [code] = |
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44890
diff
changeset
|
473 |
JType.sup_def [unfolded exec_lub_def] |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
474 |
wf_class_code |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
475 |
widen.equation |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
476 |
match_exception_entry_def |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
477 |
|
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
478 |
definition test1 where |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
479 |
"test1 = test_kil E list_name [Class list_name] (PrimT Void) 3 0 |
13092 | 480 |
[(Suc 0, 2, 8, Xcpt NullPointer)] append_ins" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
481 |
definition test2 where |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
482 |
"test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
483 |
|
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
484 |
ML {* |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
485 |
@{code test1}; |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
486 |
@{code test2}; |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
41413
diff
changeset
|
487 |
*} |
13092 | 488 |
|
13006 | 489 |
end |