8388
|
1 |
(* Title: HOL/MicroJava/BV/LBVComplete.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 2000 Technische Universitaet Muenchen
|
9054
|
5 |
*)
|
8388
|
6 |
|
9054
|
7 |
header {* Completeness of the LBV *}
|
8388
|
8 |
|
9012
|
9 |
theory LBVComplete = LBVSpec:;
|
|
10 |
|
|
11 |
ML_setup {* bind_thm ("widen_RefT", widen_RefT) *};
|
|
12 |
ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *};
|
8388
|
13 |
|
|
14 |
constdefs
|
|
15 |
is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
|
|
16 |
"is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
|
|
17 |
(a!n = None \\<or> a!n = Some (b!n)))"
|
|
18 |
|
|
19 |
contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
|
|
20 |
"contains_dead ins cert phi pc \\<equiv>
|
|
21 |
(((\\<exists> branch. ins!pc = BR (Goto branch)) \\<or> ins!pc = MR Return) \\<or>
|
|
22 |
(\\<exists>mi. ins!pc = MI mi)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
|
|
23 |
cert ! (Suc pc) = Some (phi ! Suc pc)"
|
|
24 |
|
|
25 |
contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
|
|
26 |
"contains_targets ins cert phi pc \\<equiv>
|
|
27 |
\\<forall> branch. (ins!pc = BR (Goto branch) \\<or> ins!pc = BR (Ifcmpeq branch)) \\<longrightarrow>
|
|
28 |
(let pc' = nat (int pc+branch) in pc' < length phi \\<longrightarrow> cert!pc' = Some (phi!pc'))"
|
|
29 |
|
9012
|
30 |
fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
|
|
31 |
"fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
|
|
32 |
(\\<forall> pc. pc < length ins \\<longrightarrow>
|
|
33 |
contains_dead ins cert phi pc \\<and>
|
|
34 |
contains_targets ins cert phi pc)"
|
|
35 |
|
8388
|
36 |
is_target :: "[instr list, p_count] \\<Rightarrow> bool"
|
|
37 |
"is_target ins pc \\<equiv>
|
|
38 |
\\<exists> pc' branch. pc' < length ins \\<and>
|
|
39 |
(ins ! pc' = (BR (Ifcmpeq branch)) \\<or> ins ! pc' = (BR (Goto branch))) \\<and>
|
|
40 |
pc = (nat(int pc'+branch))"
|
|
41 |
|
|
42 |
maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
|
|
43 |
"maybe_dead ins pc \\<equiv>
|
|
44 |
\\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = BR (Goto branch)) \\<or>
|
|
45 |
ins!pc' = MR Return \\<or>
|
|
46 |
(\\<exists>mi. ins!pc' = MI mi))"
|
|
47 |
|
|
48 |
|
|
49 |
mdot :: "[instr list, p_count] \\<Rightarrow> bool"
|
9012
|
50 |
"mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc";
|
8388
|
51 |
|
|
52 |
|
|
53 |
consts
|
9012
|
54 |
option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list";
|
8388
|
55 |
primrec
|
|
56 |
"option_filter_n [] P n = []"
|
|
57 |
"option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1)
|
9012
|
58 |
else None # option_filter_n t P (n+1))";
|
8388
|
59 |
|
|
60 |
constdefs
|
|
61 |
option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list"
|
|
62 |
"option_filter l P \\<equiv> option_filter_n l P 0"
|
|
63 |
|
|
64 |
make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
|
|
65 |
"make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
|
|
66 |
|
|
67 |
make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
|
|
68 |
"make_Cert G Phi \\<equiv> \\<lambda> C sig.
|
|
69 |
let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
|
|
70 |
let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
|
9012
|
71 |
make_cert b (Phi C sig)";
|
8388
|
72 |
|
|
73 |
constdefs
|
|
74 |
wfprg :: "jvm_prog \\<Rightarrow> bool"
|
9012
|
75 |
"wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G";
|
|
76 |
|
|
77 |
|
|
78 |
lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l";
|
|
79 |
by (induct l) auto;
|
|
80 |
|
|
81 |
lemma is_approx_option_filter_n:
|
|
82 |
"\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a");
|
|
83 |
proof (induct a);
|
|
84 |
show "?P []"; by (auto simp add: is_approx_def);
|
|
85 |
|
|
86 |
fix l ls;
|
|
87 |
assume Cons: "?P ls";
|
|
88 |
|
|
89 |
show "?P (l#ls)";
|
|
90 |
proof (unfold is_approx_def, intro allI conjI impI);
|
|
91 |
fix n;
|
|
92 |
show "length (option_filter_n (l # ls) P n) = length (l # ls)";
|
|
93 |
by (simp only: length_ofn);
|
|
94 |
|
|
95 |
fix m;
|
|
96 |
assume "m < length (option_filter_n (l # ls) P n)";
|
|
97 |
hence m: "m < Suc (length ls)"; by (simp only: length_ofn) simp;
|
|
98 |
|
|
99 |
show "option_filter_n (l # ls) P n ! m = None \\<or>
|
|
100 |
option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)";
|
|
101 |
proof (cases "m");
|
|
102 |
assume "m = 0";
|
|
103 |
with m; show ?thesis; by simp;
|
|
104 |
next;
|
|
105 |
fix m'; assume Suc: "m = Suc m'";
|
|
106 |
from Cons;
|
|
107 |
show ?thesis;
|
|
108 |
proof (unfold is_approx_def, elim allE impE conjE);
|
|
109 |
from m Suc;
|
|
110 |
show "m' < length (option_filter_n ls P (Suc n))"; by (simp add: length_ofn);
|
|
111 |
|
|
112 |
assume "option_filter_n ls P (Suc n) ! m' = None \\<or>
|
|
113 |
option_filter_n ls P (Suc n) ! m' = Some (ls ! m')";
|
|
114 |
with m Suc;
|
|
115 |
show ?thesis; by auto;
|
|
116 |
qed;
|
|
117 |
qed;
|
|
118 |
qed;
|
|
119 |
qed;
|
|
120 |
|
|
121 |
lemma is_approx_option_filter: "is_approx (option_filter l P) l";
|
|
122 |
by (simp add: option_filter_def is_approx_option_filter_n);
|
|
123 |
|
|
124 |
lemma option_filter_Some:
|
|
125 |
"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)";
|
|
126 |
proof -;
|
|
127 |
|
|
128 |
assume 1: "n < length l" "P n";
|
|
129 |
|
|
130 |
have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)"
|
|
131 |
(is "?P l");
|
|
132 |
proof (induct l);
|
|
133 |
show "?P []"; by simp;
|
|
134 |
|
|
135 |
fix l ls; assume Cons: "?P ls";
|
|
136 |
show "?P (l#ls)";
|
|
137 |
proof (intro);
|
|
138 |
fix n n';
|
|
139 |
assume l: "n < length (l # ls)";
|
|
140 |
assume P: "P (n + n')";
|
|
141 |
show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)";
|
|
142 |
proof (cases "n");
|
|
143 |
assume "n=0";
|
|
144 |
with P; show ?thesis; by simp;
|
|
145 |
next;
|
|
146 |
fix m; assume "n = Suc m";
|
|
147 |
with l P Cons;
|
|
148 |
show ?thesis; by simp;
|
|
149 |
qed;
|
|
150 |
qed;
|
|
151 |
qed;
|
|
152 |
|
|
153 |
with 1;
|
|
154 |
show ?thesis; by (auto simp add: option_filter_def);
|
|
155 |
qed;
|
|
156 |
|
|
157 |
lemma option_filter_contains_dead:
|
|
158 |
"contains_dead ins (option_filter phi (mdot ins)) phi pc";
|
|
159 |
by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def);
|
|
160 |
|
|
161 |
lemma option_filter_contains_targets:
|
|
162 |
"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc";
|
|
163 |
proof (simp add: contains_targets_def, intro allI impI conjI);
|
|
164 |
|
|
165 |
fix branch;
|
|
166 |
assume 1: "ins ! pc = BR (Goto branch)"
|
|
167 |
"nat (int pc + branch) < length phi"
|
|
168 |
"pc < length ins";
|
|
169 |
|
|
170 |
show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))";
|
|
171 |
proof (rule option_filter_Some);
|
|
172 |
from 1; show "nat (int pc + branch) < length phi"; by simp;
|
|
173 |
from 1;
|
|
174 |
have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def);
|
|
175 |
thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def);
|
|
176 |
qed;
|
|
177 |
|
|
178 |
next;
|
|
179 |
fix branch;
|
|
180 |
assume 2: "ins ! pc = BR (Ifcmpeq branch)"
|
|
181 |
"nat (int pc + branch) < length phi"
|
|
182 |
"pc < length ins";
|
|
183 |
|
|
184 |
show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))";
|
|
185 |
proof (rule option_filter_Some);
|
|
186 |
from 2; show "nat (int pc + branch) < length phi"; by simp;
|
|
187 |
from 2;
|
|
188 |
have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def);
|
|
189 |
thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def);
|
|
190 |
qed;
|
|
191 |
|
|
192 |
qed;
|
|
193 |
|
|
194 |
|
|
195 |
lemma fits_make_cert:
|
|
196 |
"length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi";
|
|
197 |
proof -;
|
|
198 |
assume l: "length ins < length phi";
|
|
199 |
|
|
200 |
thus "fits ins (make_cert ins phi) phi";
|
|
201 |
proof (unfold fits_def make_cert_def, intro conjI allI impI);
|
|
202 |
show "is_approx (option_filter phi (mdot ins)) phi"; by (rule is_approx_option_filter);
|
|
203 |
show "length ins < length phi"; .;
|
|
204 |
|
|
205 |
fix pc;
|
|
206 |
show "contains_dead ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_dead);
|
|
207 |
|
|
208 |
assume "pc < length ins";
|
|
209 |
thus "contains_targets ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_targets);
|
|
210 |
qed;
|
|
211 |
qed;
|
|
212 |
|
|
213 |
lemma rev_surj: "\\<exists>a'. a = rev a'";
|
|
214 |
proof (induct "a");
|
|
215 |
show "\\<exists>a'. [] = rev a'"; by simp;
|
|
216 |
|
|
217 |
fix l ls; assume "\\<exists>a''. ls = rev a''";
|
|
218 |
thus "\\<exists>a'. l # ls = rev a'";
|
|
219 |
proof (elim exE);
|
|
220 |
fix a''; assume "ls = rev a''";
|
|
221 |
hence "l#ls = rev (a''@[l])"; by simp;
|
|
222 |
thus ?thesis; by blast;
|
|
223 |
qed;
|
|
224 |
qed;
|
|
225 |
|
|
226 |
lemma append_length_n: "\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x");
|
|
227 |
proof (induct "?P" "x");
|
|
228 |
show "?P []"; by simp;
|
|
229 |
|
|
230 |
fix l ls; assume Cons: "?P ls";
|
|
231 |
|
|
232 |
show "?P (l#ls)";
|
|
233 |
proof (intro allI impI);
|
|
234 |
fix n;
|
|
235 |
assume l: "n \\<le> length (l # ls)";
|
|
236 |
|
|
237 |
show "\\<exists>a b. l # ls = a @ b \\<and> length a = n";
|
|
238 |
proof (cases n);
|
|
239 |
assume "n=0"; thus ?thesis; by simp;
|
|
240 |
next;
|
|
241 |
fix "n'"; assume s: "n = Suc n'";
|
|
242 |
with l;
|
|
243 |
have "n' \\<le> length ls"; by simp;
|
|
244 |
hence "\\<exists>a b. ls = a @ b \\<and> length a = n'"; by (rule Cons [rulify]);
|
|
245 |
thus ?thesis;
|
|
246 |
proof elim;
|
|
247 |
fix a b;
|
|
248 |
assume "ls = a @ b" "length a = n'";
|
|
249 |
with s;
|
|
250 |
have "l # ls = (l#a) @ b \\<and> length (l#a) = n"; by simp;
|
|
251 |
thus ?thesis; by blast;
|
|
252 |
qed;
|
|
253 |
qed;
|
|
254 |
qed;
|
|
255 |
qed;
|
|
256 |
|
|
257 |
|
|
258 |
|
|
259 |
lemma rev_append_cons:
|
|
260 |
"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n";
|
|
261 |
proof -;
|
|
262 |
assume n: "n < length x";
|
|
263 |
hence "n \\<le> length x"; by simp;
|
|
264 |
hence "\\<exists>a b. x = a @ b \\<and> length a = n"; by (rule append_length_n [rulify]);
|
|
265 |
thus ?thesis;
|
|
266 |
proof elim;
|
|
267 |
fix r d; assume x: "x = r@d" "length r = n";
|
|
268 |
with n;
|
|
269 |
have bc: "\\<exists>b c. d = b#c"; by (simp add: neq_Nil_conv);
|
|
270 |
|
|
271 |
have "\\<exists>a. r = rev a"; by (rule rev_surj);
|
|
272 |
with bc;
|
|
273 |
show ?thesis;
|
|
274 |
proof elim;
|
|
275 |
fix a b c;
|
|
276 |
assume "r = rev a" "d = b#c";
|
|
277 |
with x;
|
|
278 |
have "x = (rev a) @ b # c \\<and> length a = n"; by simp;
|
|
279 |
thus ?thesis; by blast;
|
|
280 |
qed;
|
|
281 |
qed;
|
|
282 |
qed;
|
|
283 |
|
|
284 |
lemma widen_NT: "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
|
|
285 |
proof (cases b);
|
|
286 |
case RefT;
|
|
287 |
thus "G\\<turnstile>b\\<preceq>NT \\<Longrightarrow> b = NT"; by - (cases ref_ty, auto);
|
|
288 |
qed auto;
|
|
289 |
|
|
290 |
lemma widen_Class: "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
|
|
291 |
by (cases b) auto;
|
|
292 |
|
|
293 |
lemma all_widen_is_sup_loc:
|
|
294 |
"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
|
|
295 |
(is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a");
|
|
296 |
proof (induct "a");
|
|
297 |
show "?P []"; by simp;
|
|
298 |
|
|
299 |
fix l ls; assume Cons: "?P ls";
|
|
300 |
|
|
301 |
show "?P (l#ls)";
|
|
302 |
proof (intro allI impI);
|
|
303 |
fix b;
|
|
304 |
assume "length (l # ls) = length (b::ty list)";
|
|
305 |
with Cons;
|
|
306 |
show "?Q (l # ls) b"; by - (cases b, auto);
|
|
307 |
qed;
|
|
308 |
qed;
|
|
309 |
|
|
310 |
lemma method_inv_pseudo_mono:
|
|
311 |
"\\<lbrakk>fits ins cert phi; i = ins!pc; i = MI meth_inv; pc < length ins;
|
|
312 |
wf_prog wf_mb G; G \\<turnstile> (x, y) <=s s1; wtl_inst (ins!pc) G rT s1 s1' cert mpc pc\\<rbrakk>
|
|
313 |
\\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
|
|
314 |
((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))";
|
|
315 |
proof (cases meth_inv);
|
|
316 |
case Invoke;
|
|
317 |
assume fits: "fits ins cert phi" and
|
|
318 |
i: "i = ins ! pc" "i = MI meth_inv" and
|
|
319 |
pc: "pc < length ins" and
|
|
320 |
wfp: "wf_prog wf_mb G" and
|
|
321 |
"wtl_inst (ins!pc) G rT s1 s1' cert mpc pc" and
|
|
322 |
lt: "G \\<turnstile> (x, y) <=s s1";
|
|
323 |
|
|
324 |
with Invoke;
|
|
325 |
show ?thesis; (* (is "\\<exists>s2'. ?wtl s2' \\<and> (?lt s2' s1' \\<or> ?cert s2')" is "\\<exists>s2'. ?P s2'"); *)
|
|
326 |
proof (clarsimp_tac simp del: split_paired_Ex);
|
|
327 |
fix apTs X ST' y' s;
|
|
328 |
|
|
329 |
assume G: "G \\<turnstile> (x, y) <=s (rev apTs @ X # ST', y')";
|
|
330 |
assume lapTs: "length apTs = length list";
|
|
331 |
assume "cert ! Suc pc = Some s";
|
|
332 |
assume wtl: "s = s1' \\<and> X = NT \\<or>
|
|
333 |
G \\<turnstile> s1' <=s s \\<and>
|
|
334 |
(\\<exists>C. X = Class C \\<and>
|
|
335 |
(\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
|
|
336 |
(\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and>
|
|
337 |
(rT # ST', y') = s1'))" (is "?NT \\<or> ?ClassC");
|
|
338 |
|
|
339 |
from G;
|
|
340 |
have "\\<exists>a b c. x = rev a @ b # c \\<and> length a = length apTs";
|
|
341 |
by - (rule rev_append_cons, simp add: sup_state_length_fst);
|
|
342 |
|
|
343 |
thus "\\<exists>s2'. (\\<exists>apTs X ST'.
|
|
344 |
x = rev apTs @ X # ST' \\<and>
|
|
345 |
length apTs = length list \\<and>
|
|
346 |
(s = s2' \\<and> X = NT \\<or>
|
|
347 |
G \\<turnstile> s2' <=s s \\<and>
|
|
348 |
(\\<exists>C. X = Class C \\<and>
|
|
349 |
(\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
|
|
350 |
(\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and>
|
|
351 |
(rT # ST', y) = s2')))) \\<and>
|
|
352 |
(G \\<turnstile> s2' <=s s1' \\<or> G \\<turnstile> s2' <=s s)" (is "\\<exists>s2'. ?P s2'");
|
|
353 |
proof elim;
|
|
354 |
fix a b c;
|
|
355 |
assume rac: "x = rev a @ b # c";
|
|
356 |
with G;
|
|
357 |
have x: "G \\<turnstile> (rev a @ b # c, y) <=s (rev apTs @ X # ST', y')"; by simp;
|
|
358 |
|
|
359 |
assume l: "length a = length apTs";
|
|
360 |
hence "length (rev a) = length (rev apTs)"; by simp;
|
|
361 |
|
|
362 |
with x;
|
|
363 |
have "G \\<turnstile> (rev a, y) <=s (rev apTs, y') \\<and> G \\<turnstile> (b # c, y) <=s (X # ST', y')";
|
|
364 |
by - (rule sup_state_append_fst [elimify], blast+);
|
|
365 |
|
|
366 |
hence x2: "G \\<turnstile> (a, y) <=s (apTs, y') \\<and> G \\<turnstile> b\\<preceq>X \\<and> G \\<turnstile> (c, y) <=s (ST', y')";
|
|
367 |
by (simp add: sup_state_rev_fst sup_state_Cons1);
|
|
368 |
|
|
369 |
show ?thesis;
|
|
370 |
proof (cases "X = NT");
|
|
371 |
case True;
|
|
372 |
with x2;
|
|
373 |
have "b = NT"; by (clarsimp_tac simp add: widen_NT);
|
|
374 |
|
|
375 |
with rac l lapTs;
|
|
376 |
have "?P s"; by auto;
|
|
377 |
thus ?thesis; by blast;
|
|
378 |
|
|
379 |
next;
|
|
380 |
case False;
|
|
381 |
|
|
382 |
with wtl;
|
|
383 |
have "\\<exists>C. X = Class C"; by clarsimp_tac;
|
|
384 |
with x2;
|
|
385 |
have "\\<exists>r. b = RefT r"; by (auto simp add: widen_Class);
|
|
386 |
|
|
387 |
thus ?thesis;
|
|
388 |
proof elim;
|
|
389 |
fix r;
|
|
390 |
assume b: "b = RefT r";
|
|
391 |
show ?thesis;
|
|
392 |
proof (cases r);
|
|
393 |
case NullT;
|
|
394 |
with b rac x2 l lapTs wtl False;
|
|
395 |
have "?P s"; by auto;
|
|
396 |
thus ?thesis; by blast;
|
|
397 |
next;
|
|
398 |
case ClassT;
|
|
399 |
|
|
400 |
from False wtl;
|
|
401 |
have wtlC: "?ClassC"; by simp;
|
|
402 |
|
|
403 |
with b ClassT;
|
|
404 |
show ?thesis;
|
|
405 |
proof (elim exE conjE);
|
|
406 |
fix C D rT body;
|
|
407 |
assume ClassC: "X = Class C";
|
|
408 |
assume zip: "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G";
|
|
409 |
assume s1': "(rT # ST', y') = s1'";
|
|
410 |
assume s: "G \\<turnstile> s1' <=s s";
|
|
411 |
assume method: "method (G, C) (mname, list) = Some (D, rT, body)";
|
|
412 |
|
|
413 |
from ClassC b ClassT x2;
|
|
414 |
have "G \\<turnstile> cname \\<preceq>C C"; by simp;
|
|
415 |
with method wfp;
|
|
416 |
have "\\<exists>D' rT' b'. method (G, cname) (mname, list) = Some (D', rT', b') \\<and> G \\<turnstile> rT'\\<preceq>rT";
|
|
417 |
by - (rule subcls_widen_methd, blast);
|
|
418 |
|
|
419 |
thus ?thesis;
|
|
420 |
proof elim;
|
|
421 |
fix D' rT' body';
|
|
422 |
assume method': "method (G, cname) (mname, list) = Some (D', rT', body')" "G\\<turnstile>rT'\\<preceq>rT";
|
|
423 |
|
|
424 |
have "?P (rT'#c,y)" (is "(\\<exists> apTs X ST'. ?A apTs X ST') \\<and> ?B");
|
|
425 |
proof (intro conjI);
|
|
426 |
from s1' method' x2;
|
|
427 |
show "?B"; by (auto simp add: sup_state_Cons1);
|
|
428 |
|
|
429 |
from b ClassT rac l lapTs method';
|
|
430 |
have "?A a (Class cname) c";
|
|
431 |
proof (simp, intro conjI);
|
|
432 |
|
|
433 |
from method' x2;
|
|
434 |
have s': "G \\<turnstile> (rT' # c, y) <=s (rT # ST', y')";
|
|
435 |
by (auto simp add: sup_state_Cons1);
|
|
436 |
from s s1';
|
|
437 |
have "G \\<turnstile> (rT # ST', y') <=s s"; by simp;
|
|
438 |
with s';
|
|
439 |
show "G \\<turnstile> (rT' # c, y) <=s s"; by (rule sup_state_trans);
|
|
440 |
|
|
441 |
from x2;
|
|
442 |
have 1: "G \\<turnstile> map Some a <=l map Some apTs"; by (simp add: sup_state_def);
|
|
443 |
from lapTs zip;
|
|
444 |
have "G \\<turnstile> map Some apTs <=l map Some list"; by (simp add: all_widen_is_sup_loc);
|
|
445 |
with 1;
|
|
446 |
have "G \\<turnstile> map Some a <=l map Some list"; by (rule sup_loc_trans);
|
|
447 |
with l lapTs;
|
|
448 |
show "\\<forall>x\\<in>set (zip a list). x \\<in> widen G"; by (simp add: all_widen_is_sup_loc);
|
|
449 |
|
|
450 |
qed;
|
|
451 |
thus "\\<exists> apTs X ST'. ?A apTs X ST'"; by blast;
|
|
452 |
qed;
|
|
453 |
thus ?thesis; by blast;
|
|
454 |
qed;
|
|
455 |
qed;
|
|
456 |
qed;
|
|
457 |
qed;
|
|
458 |
qed;
|
|
459 |
qed;
|
|
460 |
qed;
|
|
461 |
qed;
|
|
462 |
|
|
463 |
lemma sup_loc_some:
|
|
464 |
"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b");
|
|
465 |
proof (induct "?P" b);
|
|
466 |
show "?P []"; by simp;
|
|
467 |
|
|
468 |
case Cons;
|
|
469 |
show "?P (a#list)";
|
|
470 |
proof (clarsimp_tac simp add: list_all2_Cons1 sup_loc_def);
|
|
471 |
fix z zs n;
|
|
472 |
assume * :
|
|
473 |
"G \\<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
|
|
474 |
"n < Suc (length zs)" "(z # zs) ! n = Some t";
|
|
475 |
|
|
476 |
show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t";
|
|
477 |
proof (cases n);
|
|
478 |
case 0;
|
|
479 |
with *; show ?thesis; by (simp add: sup_ty_opt_some);
|
|
480 |
next;
|
|
481 |
case Suc;
|
|
482 |
with Cons *;
|
|
483 |
show ?thesis; by (simp add: sup_loc_def);
|
|
484 |
qed;
|
|
485 |
qed;
|
|
486 |
qed;
|
|
487 |
|
|
488 |
lemma mono_load:
|
|
489 |
"\\<lbrakk>G \\<turnstile> (a, b) <=s (x, y); n < length y; y!n = Some t\\<rbrakk> \\<Longrightarrow> \\<exists>ts. b!n = Some ts \\<and> G \\<turnstile> (ts#a, b) <=s (t#x, y)";
|
|
490 |
proof (clarsimp_tac simp add: sup_state_def);
|
|
491 |
assume "G \\<turnstile> b <=l y" "n < length y" "y!n = Some t";
|
|
492 |
thus "\\<exists>ts. b ! n = Some ts \\<and> G\\<turnstile>ts\\<preceq>t";
|
|
493 |
by (rule sup_loc_some [rulify, elimify], clarsimp_tac);
|
|
494 |
qed;
|
|
495 |
|
|
496 |
lemma mono_store:
|
|
497 |
"\\<lbrakk>G \\<turnstile> (a, b) <=s (ts # ST', y); n < length y\\<rbrakk> \\<Longrightarrow>
|
|
498 |
\\<exists> t a'. a = t#a' \\<and> G \\<turnstile> (a', b[n := Some t]) <=s (ST', y[n := Some ts])";
|
|
499 |
proof (clarsimp_tac simp add: sup_state_def sup_loc_Cons2);
|
|
500 |
fix Y YT';
|
|
501 |
assume * : "n < length y" "G \\<turnstile> b <=l y" "G \\<turnstile>Y <=o Some ts" "G \\<turnstile> YT' <=l map Some ST'";
|
|
502 |
assume "map Some a = Y # YT'";
|
|
503 |
hence "map Some (tl a) = YT' \\<and> Some (hd a) = Y \\<and> (\\<exists>y yt. a = y # yt)";
|
|
504 |
by (rule map_hd_tl);
|
|
505 |
with *;
|
|
506 |
show "\\<exists>t a'. a = t # a' \\<and> G \\<turnstile> map Some a' <=l map Some ST' \\<and> G \\<turnstile> b[n := Some t] <=l y[n := Some ts]";
|
|
507 |
by (clarsimp_tac simp add: sup_loc_update);
|
|
508 |
qed;
|
|
509 |
|
|
510 |
|
|
511 |
lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
|
|
512 |
proof;
|
|
513 |
show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p"; by blast;
|
|
514 |
|
|
515 |
show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p";
|
|
516 |
proof (cases xb); print_cases;
|
|
517 |
fix prim;
|
|
518 |
assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p";
|
|
519 |
thus ?thesis; by simp;
|
|
520 |
next;
|
|
521 |
fix ref;
|
|
522 |
assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref";
|
|
523 |
thus ?thesis; by simp (rule widen_RefT [elimify], auto);
|
|
524 |
qed;
|
|
525 |
qed;
|
|
526 |
|
|
527 |
|
|
528 |
lemma wtl_inst_pseudo_mono:
|
|
529 |
"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G;
|
|
530 |
G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
|
|
531 |
\\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
|
|
532 |
proof (simp only:);
|
|
533 |
assume 1 : "wtl_inst (ins ! pc) G rT s1 s1' cert mpc pc" "G \\<turnstile> s2 <=s s1" "pc < length ins";
|
|
534 |
assume 2 : "fits ins cert phi" "wf_prog wf_mb G" "i = ins!pc";
|
|
535 |
|
|
536 |
have 3: "\\<exists> a b. s2 = (a,b)"; by simp;
|
|
537 |
|
|
538 |
show ?thesis;
|
|
539 |
proof (cases "ins ! pc");
|
|
540 |
|
|
541 |
case LS;
|
|
542 |
show ?thesis;
|
|
543 |
proof (cases "load_and_store");
|
|
544 |
case Load;
|
|
545 |
with LS 1 3;
|
|
546 |
show ?thesis; by (elim, clarsimp_tac) (rule mono_load [elimify], auto simp add: sup_state_length_snd);
|
|
547 |
next;
|
|
548 |
case Store;
|
|
549 |
with LS 1 3;
|
|
550 |
show ?thesis; by (elim, clarsimp_tac) (rule mono_store [elimify], auto simp add: sup_state_length_snd);
|
|
551 |
next;
|
|
552 |
case Bipush;
|
|
553 |
with LS 1 3;
|
|
554 |
show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
|
|
555 |
next;
|
|
556 |
case Aconst_null;
|
|
557 |
with LS 1 3;
|
|
558 |
show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
|
|
559 |
qed;
|
|
560 |
|
|
561 |
next;
|
|
562 |
case CO;
|
|
563 |
show ?thesis;
|
|
564 |
proof (cases create_object);
|
|
565 |
case New;
|
|
566 |
with CO 1 3;
|
|
567 |
show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
|
|
568 |
qed;
|
|
569 |
|
|
570 |
next;
|
|
571 |
case MO;
|
|
572 |
show ?thesis;
|
|
573 |
proof (cases manipulate_object);
|
|
574 |
case Getfield;
|
|
575 |
with MO 1 3;
|
|
576 |
show ?thesis;
|
|
577 |
proof (elim, clarsimp_tac simp add: sup_state_Cons2);
|
|
578 |
fix oT x;
|
|
579 |
assume "G \\<turnstile> x \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
|
|
580 |
show "G \\<turnstile> x \\<preceq> Class cname"; by (rule widen_trans);
|
|
581 |
qed;
|
|
582 |
next;
|
|
583 |
case Putfield;
|
|
584 |
with MO 1 3;
|
|
585 |
show ?thesis;
|
|
586 |
proof (elim, clarsimp_tac simp add: sup_state_Cons2);
|
|
587 |
fix x xa vT oT T;
|
|
588 |
assume "G \\<turnstile> x \\<preceq> vT" "G \\<turnstile> vT \\<preceq> T";
|
|
589 |
hence * : "G \\<turnstile> x \\<preceq> T"; by (rule widen_trans);
|
|
590 |
|
|
591 |
assume "G \\<turnstile> xa \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
|
|
592 |
hence "G \\<turnstile> xa \\<preceq> Class cname"; by (rule widen_trans);
|
|
593 |
|
|
594 |
with *;
|
|
595 |
show "(G \\<turnstile> xa \\<preceq> Class cname) \\<and> (G \\<turnstile> x \\<preceq> T)"; by blast;
|
|
596 |
qed;
|
|
597 |
qed;
|
|
598 |
|
|
599 |
next;
|
|
600 |
case CH;
|
|
601 |
show ?thesis;
|
|
602 |
proof (cases check_object);
|
|
603 |
case Checkcast;
|
|
604 |
with CH 1 3;
|
|
605 |
show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons2) (rule widen_RefT2);
|
|
606 |
qed;
|
|
607 |
|
|
608 |
next;
|
|
609 |
case MI;
|
|
610 |
with 1 2 3;
|
|
611 |
show ?thesis; by elim (rule method_inv_pseudo_mono [elimify], simp+);
|
8388
|
612 |
|
9012
|
613 |
next;
|
|
614 |
case MR;
|
|
615 |
show ?thesis;
|
|
616 |
proof (cases meth_ret);
|
|
617 |
case Return;
|
|
618 |
with MR 1 3;
|
|
619 |
show ?thesis;
|
|
620 |
proof (elim, clarsimp_tac simp add: sup_state_Cons2 simp del: split_paired_Ex);
|
|
621 |
fix x T;
|
|
622 |
assume "G\\<turnstile>x\\<preceq>T" "G\\<turnstile>T\\<preceq>rT";
|
|
623 |
thus "G\\<turnstile>x\\<preceq>rT"; by (rule widen_trans);
|
|
624 |
qed;
|
|
625 |
qed;
|
|
626 |
|
|
627 |
next;
|
|
628 |
case OS;
|
|
629 |
with 1 3;
|
|
630 |
show ?thesis;
|
|
631 |
by - (cases op_stack, (elim, clarsimp_tac simp add: sup_state_Cons2)+);
|
|
632 |
|
|
633 |
next;
|
|
634 |
case BR;
|
|
635 |
show ?thesis;
|
|
636 |
proof (cases branch);
|
|
637 |
case Goto;
|
|
638 |
with BR 1 3;
|
|
639 |
show ?thesis;
|
|
640 |
proof (elim, clarsimp_tac simp del: split_paired_Ex);
|
|
641 |
fix a b x y;
|
|
642 |
assume "G \\<turnstile> (a, b) <=s s1" "G \\<turnstile> s1 <=s (x, y)";
|
|
643 |
thus "G \\<turnstile> (a, b) <=s (x, y)"; by (rule sup_state_trans);
|
|
644 |
qed;
|
|
645 |
next;
|
|
646 |
case Ifcmpeq;
|
|
647 |
with BR 1 3;
|
|
648 |
show ?thesis;
|
|
649 |
proof (elim, clarsimp_tac simp add: sup_state_Cons2, intro conjI);
|
|
650 |
fix xt' b ST' y c d;
|
|
651 |
assume "G \\<turnstile> (xt', b) <=s (ST', y)" "G \\<turnstile> (ST', y) <=s (c, d)";
|
|
652 |
thus "G \\<turnstile> (xt', b) <=s (c, d)"; by (rule sup_state_trans);
|
|
653 |
next;
|
|
654 |
fix ts ts' x xa;
|
|
655 |
assume * :
|
|
656 |
"(\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or> (\\<exists>r. ts = RefT r) \\<and> (\\<exists>r'. ts' = RefT r')";
|
|
657 |
|
|
658 |
assume x: "G\\<turnstile>x\\<preceq>ts" "G\\<turnstile>xa\\<preceq>ts'";
|
|
659 |
|
|
660 |
show "(\\<exists>p. x = PrimT p \\<and> xa = PrimT p) \\<or> (\\<exists>r. x = RefT r) \\<and> (\\<exists>r'. xa = RefT r')";
|
|
661 |
proof (cases x);
|
|
662 |
case PrimT;
|
|
663 |
with * x;
|
|
664 |
show ?thesis; by (auto simp add: PrimT_PrimT);
|
|
665 |
next;
|
|
666 |
case RefT;
|
|
667 |
hence 1: "\\<exists>r. x = RefT r"; by blast;
|
|
668 |
|
|
669 |
have "\\<exists>r'. xa = RefT r'";
|
|
670 |
proof (cases xa);
|
|
671 |
case PrimT;
|
|
672 |
with RefT * x;
|
|
673 |
have "False"; by auto (rule widen_RefT [elimify], auto);
|
|
674 |
thus ?thesis; by blast;
|
|
675 |
qed blast;
|
|
676 |
|
|
677 |
with 1;
|
|
678 |
show ?thesis; by blast;
|
|
679 |
qed;
|
|
680 |
qed;
|
|
681 |
qed;
|
|
682 |
qed;
|
|
683 |
qed;
|
|
684 |
|
|
685 |
lemma wtl_inst_last_mono:
|
|
686 |
"\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
|
|
687 |
\\<exists>s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
|
|
688 |
proof -;
|
|
689 |
assume * : "wtl_inst i G rT s1 s1' cert (Suc pc) pc" "G \\<turnstile> s2 <=s s1";
|
|
690 |
|
|
691 |
show ?thesis;
|
|
692 |
proof (cases i);
|
|
693 |
case LS; with *;
|
|
694 |
show ?thesis; by - (cases load_and_store, simp+);
|
|
695 |
next;
|
|
696 |
case CO; with *;
|
|
697 |
show ?thesis; by - (cases create_object, simp);
|
|
698 |
next;
|
|
699 |
case MO; with *;
|
|
700 |
show ?thesis; by - (cases manipulate_object, simp+);
|
|
701 |
next;
|
|
702 |
case CH; with *;
|
|
703 |
show ?thesis; by - (cases check_object, simp);
|
|
704 |
next;
|
|
705 |
case MI; with *;
|
|
706 |
show ?thesis; by - (cases meth_inv, simp);
|
|
707 |
next;
|
|
708 |
case OS; with *;
|
|
709 |
show ?thesis; by - (cases op_stack, simp+);
|
|
710 |
next;
|
|
711 |
case MR;
|
|
712 |
show ?thesis;
|
|
713 |
proof (cases meth_ret);
|
|
714 |
case Return; with MR *;
|
|
715 |
show ?thesis;
|
|
716 |
by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
|
|
717 |
(rule widen_trans, blast+);
|
|
718 |
qed;
|
|
719 |
next;
|
|
720 |
case BR;
|
|
721 |
show ?thesis;
|
|
722 |
proof (cases branch);
|
|
723 |
case Ifcmpeq; with BR *;
|
|
724 |
show ?thesis; by simp;
|
|
725 |
next;
|
|
726 |
case Goto; with BR *;
|
|
727 |
show ?thesis;
|
|
728 |
by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
|
|
729 |
(rule sup_state_trans, blast+);
|
|
730 |
qed;
|
|
731 |
qed;
|
|
732 |
qed;
|
|
733 |
|
|
734 |
lemma wtl_option_last_mono:
|
|
735 |
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; mpc = Suc pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
|
|
736 |
\\<exists>s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
|
|
737 |
proof (simp only: );
|
|
738 |
assume G: "G \\<turnstile> s2 <=s s1";
|
|
739 |
assume w: "wtl_inst_option i G rT s1 s1' cert (Suc pc) pc";
|
|
740 |
|
|
741 |
show "\\<exists>s2'. wtl_inst_option i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
|
|
742 |
proof (cases "cert!pc");
|
|
743 |
case None;
|
|
744 |
with G w;
|
|
745 |
show ?thesis; by (simp add: wtl_inst_option_def wtl_inst_last_mono del: split_paired_Ex);
|
|
746 |
next;
|
|
747 |
case Some;
|
|
748 |
with G w;
|
|
749 |
have o: "G \\<turnstile> s1 <=s a \\<and> wtl_inst i G rT a s1' cert (Suc pc) pc";
|
|
750 |
by (simp add: wtl_inst_option_def);
|
|
751 |
hence w' : "wtl_inst i G rT a s1' cert (Suc pc) pc"; ..;
|
|
752 |
|
|
753 |
from o G;
|
|
754 |
have G' : "G \\<turnstile> s2 <=s a"; by - (rule sup_state_trans, blast+);
|
|
755 |
|
|
756 |
from o;
|
|
757 |
have "\\<exists>s2'. wtl_inst i G rT a s2' cert (Suc pc) pc \\<and> G \\<turnstile> s2' <=s s1'";
|
|
758 |
by elim (rule wtl_inst_last_mono, auto);
|
|
759 |
|
|
760 |
with Some w G';
|
|
761 |
show ?thesis; by (auto simp add: wtl_inst_option_def);
|
|
762 |
qed;
|
|
763 |
qed;
|
|
764 |
|
|
765 |
lemma wt_instr_imp_wtl_inst:
|
|
766 |
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
|
|
767 |
pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow>
|
|
768 |
\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
|
|
769 |
proof -;
|
|
770 |
assume * : "wt_instr (ins!pc) G rT phi max_pc pc" "fits ins cert phi"
|
|
771 |
"pc < length ins" "length ins = max_pc";
|
|
772 |
|
|
773 |
have xy: "\\<exists> x y. phi!pc = (x,y)"; by simp;
|
|
774 |
|
|
775 |
show ?thesis;
|
|
776 |
proof (cases "ins!pc");
|
|
777 |
case LS; with * xy;
|
|
778 |
show ?thesis;
|
|
779 |
by - (cases load_and_store, (elim, force simp add: wt_instr_def)+);
|
|
780 |
next;
|
|
781 |
case CO; with * xy;
|
|
782 |
show ?thesis;
|
|
783 |
by - (cases create_object, (elim, force simp add: wt_instr_def)+);
|
|
784 |
next;
|
|
785 |
case MO; with * xy;
|
|
786 |
show ?thesis;
|
|
787 |
by - (cases manipulate_object, (elim, force simp add: wt_instr_def)+);
|
|
788 |
next;
|
|
789 |
case CH; with * xy;
|
|
790 |
show ?thesis;
|
|
791 |
by - (cases check_object, (elim, force simp add: wt_instr_def)+);
|
|
792 |
next;
|
|
793 |
case OS; with * xy;
|
|
794 |
show ?thesis;
|
|
795 |
by - (cases op_stack, (elim, force simp add: wt_instr_def)+);
|
|
796 |
next;
|
|
797 |
case MR; with * xy;
|
|
798 |
show ?thesis;
|
|
799 |
by - (cases meth_ret, elim,
|
|
800 |
clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def simp del: split_paired_Ex);
|
|
801 |
next;
|
|
802 |
case BR; with * xy;
|
|
803 |
show ?thesis;
|
|
804 |
by - (cases branch,
|
|
805 |
(clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def contains_targets_def
|
|
806 |
simp del: split_paired_Ex)+);
|
|
807 |
next;
|
|
808 |
case MI;
|
|
809 |
show ?thesis;
|
|
810 |
proof (cases meth_inv);
|
|
811 |
case Invoke;
|
|
812 |
with MI * xy;
|
|
813 |
show ?thesis;
|
|
814 |
proof (elim, clarsimp_tac simp add: wt_instr_def simp del: split_paired_Ex);
|
|
815 |
fix y apTs X ST';
|
|
816 |
assume pc : "Suc pc < length ins";
|
|
817 |
assume phi : "phi ! pc = (rev apTs @ X # ST', y)" "length apTs = length list";
|
|
818 |
assume ** :
|
|
819 |
"X = NT \\<or> (\\<exists>C. X = Class C \\<and>
|
|
820 |
(\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
|
|
821 |
(\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc))"
|
|
822 |
(is "?NT \\<or> ?CL");
|
|
823 |
|
|
824 |
|
|
825 |
from MI Invoke pc *;
|
|
826 |
have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def);
|
|
827 |
|
|
828 |
|
|
829 |
show "\\<exists>s. (\\<exists>apTsa Xa ST'a.
|
|
830 |
rev apTs @ X # ST' = rev apTsa @ Xa # ST'a \\<and>
|
|
831 |
length apTsa = length list \\<and>
|
|
832 |
(\\<exists>s''. cert ! Suc pc = Some s'' \\<and>
|
|
833 |
(s'' = s \\<and> Xa = NT \\<or>
|
|
834 |
G \\<turnstile> s <=s s'' \\<and>
|
|
835 |
(\\<exists>C. Xa = Class C \\<and>
|
|
836 |
(\\<forall>x\\<in>set (zip apTsa list). x \\<in> widen G) \\<and>
|
|
837 |
(\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> (rT # ST'a, y) = s))))) \\<and>
|
|
838 |
G \\<turnstile> s <=s phi ! Suc pc" (is "\\<exists>s. ?P s");
|
|
839 |
proof (cases "X=NT");
|
|
840 |
case True;
|
|
841 |
with cert phi **;
|
|
842 |
have "?P (phi ! Suc pc)"; by (force simp del: split_paired_Ex);
|
|
843 |
thus ?thesis; by blast;
|
|
844 |
next;
|
|
845 |
case False;
|
|
846 |
with **;
|
|
847 |
|
|
848 |
have "?CL"; by simp;
|
|
849 |
|
|
850 |
thus ?thesis;
|
|
851 |
proof (elim exE conjE);
|
|
852 |
fix C D rT b;
|
|
853 |
assume "X = Class C" "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G"
|
|
854 |
"G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc"
|
|
855 |
"method (G, C) (mname, list) = Some (D, rT, b)";
|
|
856 |
with cert phi;
|
|
857 |
have "?P (rT #ST', y)"; by (force simp del: split_paired_Ex);
|
|
858 |
thus ?thesis; by blast;
|
|
859 |
qed;
|
|
860 |
qed;
|
|
861 |
qed;
|
|
862 |
qed;
|
|
863 |
qed;
|
|
864 |
qed;
|
|
865 |
|
|
866 |
|
|
867 |
lemma wt_instr_imp_wtl_option:
|
|
868 |
"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\\<rbrakk> \\<Longrightarrow>
|
|
869 |
\\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
|
|
870 |
proof -;
|
|
871 |
assume fits : "fits ins cert phi" "pc < length ins"
|
|
872 |
and "wt_instr (ins!pc) G rT phi max_pc pc"
|
|
873 |
"max_pc = length ins";
|
|
874 |
|
|
875 |
hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
|
|
876 |
by - (rule wt_instr_imp_wtl_inst, simp+);
|
|
877 |
|
|
878 |
show ?thesis;
|
|
879 |
proof (cases "cert ! pc");
|
|
880 |
case None;
|
|
881 |
with *;
|
|
882 |
show ?thesis; by (simp add: wtl_inst_option_def);
|
|
883 |
|
|
884 |
next;
|
|
885 |
case Some;
|
|
886 |
|
|
887 |
from fits;
|
|
888 |
have "pc < length phi"; by (clarsimp_tac simp add: fits_def);
|
|
889 |
with fits Some;
|
|
890 |
have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
|
|
891 |
|
|
892 |
with *;
|
|
893 |
show ?thesis; by (simp add: wtl_inst_option_def);
|
|
894 |
qed;
|
|
895 |
qed;
|
|
896 |
|
|
897 |
(* not needed
|
|
898 |
lemma wtl_inst_list_s:
|
|
899 |
"\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; ins \\<noteq> []; G \\<turnstile> s <=s s0; s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow>
|
|
900 |
wtl_inst_list ins G rT s s' cert max_pc pc";
|
|
901 |
proof -;
|
|
902 |
assume * : "wtl_inst_list ins G rT s0 s' cert max_pc pc"
|
|
903 |
"ins \\<noteq> []" "G \\<turnstile> s <=s s0"
|
|
904 |
"s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0";
|
|
905 |
|
|
906 |
show ?thesis;
|
|
907 |
proof (cases ins);
|
|
908 |
case Nil;
|
|
909 |
with *;
|
|
910 |
show ?thesis; by simp;
|
|
911 |
next;
|
|
912 |
case Cons;
|
|
913 |
|
|
914 |
show ?thesis;
|
|
915 |
proof (cases "list = []");
|
|
916 |
case True;
|
|
917 |
with Cons *;
|
|
918 |
show ?thesis; by - (cases "s = s0", (simp add: wtl_inst_option_def)+);
|
|
919 |
next;
|
|
920 |
case False;
|
|
921 |
with Cons *;
|
|
922 |
show ?thesis; by (force simp add: wtl_inst_option_def);
|
|
923 |
qed;
|
|
924 |
qed;
|
|
925 |
qed;
|
|
926 |
|
|
927 |
|
|
928 |
lemma wtl_inst_list_cert:
|
|
929 |
"\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow>
|
|
930 |
wtl_inst_list ins G rT s s' cert max_pc pc";
|
|
931 |
by (cases ins) (force simp add: wtl_inst_option_def)+;
|
|
932 |
*)
|
|
933 |
|
|
934 |
lemma wtl_option_pseudo_mono:
|
|
935 |
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
|
|
936 |
wf_prog wf_mb G; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
|
|
937 |
\\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and>
|
|
938 |
(G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
|
|
939 |
proof -;
|
|
940 |
assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and
|
|
941 |
fits: "fits ins cert phi" "pc < length ins"
|
|
942 |
"wf_prog wf_mb G" "G \\<turnstile> s2 <=s s1" "i = ins!pc";
|
|
943 |
|
|
944 |
show ?thesis;
|
|
945 |
proof (cases "cert!pc");
|
|
946 |
case None;
|
|
947 |
with wtl fits;
|
|
948 |
show ?thesis;
|
|
949 |
by - (rule wtl_inst_pseudo_mono [elimify], (simp add: wtl_inst_option_def)+);
|
|
950 |
next;
|
|
951 |
case Some;
|
|
952 |
with wtl fits;
|
|
953 |
|
|
954 |
have G: "G \\<turnstile> s2 <=s a";
|
|
955 |
by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+);
|
|
956 |
|
|
957 |
from Some wtl;
|
|
958 |
have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def);
|
|
959 |
|
|
960 |
with G fits;
|
|
961 |
have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and>
|
|
962 |
(G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
|
|
963 |
by - (rule wtl_inst_pseudo_mono, (simp add: wtl_inst_option_def)+);
|
|
964 |
|
|
965 |
with Some G;
|
|
966 |
show ?thesis; by (simp add: wtl_inst_option_def);
|
|
967 |
qed;
|
|
968 |
qed;
|
|
969 |
|
|
970 |
lemma append_cons_length_nth: "((l @ a # list) ! length l) = a";
|
|
971 |
by (induct l, auto);
|
|
972 |
|
|
973 |
|
|
974 |
(* main induction over instruction list *)
|
|
975 |
theorem wt_imp_wtl_inst_list:
|
|
976 |
"\\<forall> pc. (\\<forall>pc'. pc' < length ins \\<longrightarrow> wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\<longrightarrow>
|
|
977 |
wf_prog wf_mb G \\<longrightarrow>
|
|
978 |
fits all_ins cert phi \\<longrightarrow> (\\<exists> l. pc = length l \\<and> all_ins=l@ins) \\<longrightarrow> pc < length all_ins \\<longrightarrow>
|
|
979 |
(\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow>
|
|
980 |
(\\<exists>s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))"
|
|
981 |
(is "\\<forall>pc. ?C pc ins" is "?P ins");
|
|
982 |
proof (induct "?P" "ins");
|
|
983 |
case Nil;
|
|
984 |
show "?P []"; by simp;
|
|
985 |
next;
|
|
986 |
case Cons;
|
|
987 |
|
|
988 |
show "?P (a#list)";
|
|
989 |
proof (intro allI impI, elim exE conjE);
|
|
990 |
fix pc s l;
|
|
991 |
assume 1: "wf_prog wf_mb G" "fits all_ins cert phi";
|
|
992 |
assume 2: "pc < length all_ins" "G \\<turnstile> s <=s phi ! pc"
|
|
993 |
"all_ins = l @ a # list" "pc = length l";
|
|
994 |
|
|
995 |
from Cons;
|
|
996 |
have IH: "?C (Suc pc) list"; by blast;
|
|
997 |
|
|
998 |
assume 3: "\\<forall>pc'. pc' < length (a # list) \\<longrightarrow>
|
|
999 |
wt_instr ((a # list) ! pc') G rT phi (pc + length (a # list)) (pc + pc')";
|
|
1000 |
hence 4: "\\<forall>pc'. pc' < length list \\<longrightarrow>
|
|
1001 |
wt_instr (list ! pc') G rT phi (Suc pc + length list) (Suc pc + pc')"; by auto;
|
|
1002 |
|
|
1003 |
from 2;
|
|
1004 |
have 5: "a = all_ins ! pc"; by (simp add: append_cons_length_nth);
|
|
1005 |
|
|
1006 |
|
|
1007 |
show "\\<exists>s'. wtl_inst_list (a # list) G rT s s' cert (pc + length (a # list)) pc";
|
|
1008 |
proof (cases list);
|
|
1009 |
case Nil;
|
|
1010 |
|
|
1011 |
with 1 2 3 5;
|
|
1012 |
have "\\<exists>s'. wtl_inst_option a G rT (phi ! pc) s' cert (Suc (length l)) pc";
|
|
1013 |
by - (rule wt_instr_imp_wtl_option [elimify], force+);
|
|
1014 |
|
|
1015 |
with Nil 1 2 5;
|
|
1016 |
have "\\<exists>s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc";
|
|
1017 |
by elim (rule wtl_option_pseudo_mono [elimify], force+);
|
|
1018 |
|
|
1019 |
with Nil 2;
|
|
1020 |
show ?thesis; by auto;
|
|
1021 |
next;
|
|
1022 |
fix i' ins';
|
|
1023 |
assume Cons2: "list = i' # ins'";
|
|
1024 |
|
|
1025 |
with IH 1 2 3;
|
|
1026 |
have * : "\\<forall> s. (G \\<turnstile> s <=s (phi!(Suc pc))) \\<longrightarrow>
|
|
1027 |
(\\<exists>s'. wtl_inst_list list G rT s s' cert ((Suc pc)+length list) (Suc pc))";
|
|
1028 |
by (elim impE) force+;
|
|
1029 |
|
|
1030 |
from 3;
|
|
1031 |
have "wt_instr a G rT phi (pc + length (a # list)) pc"; by auto;
|
|
1032 |
|
|
1033 |
with 1 2 5;
|
|
1034 |
have "\\<exists>s1'. wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc \\<and> G \\<turnstile> s1' <=s phi ! Suc pc";
|
|
1035 |
by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+);
|
|
1036 |
|
|
1037 |
hence "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
|
|
1038 |
(G \\<turnstile> s1 <=s (phi ! (Suc pc)) \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))";
|
|
1039 |
proof elim;
|
|
1040 |
fix s1';
|
|
1041 |
assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and
|
|
1042 |
a :"G \\<turnstile> s1' <=s phi ! Suc pc";
|
|
1043 |
with 1 2 5;
|
|
1044 |
have "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
|
|
1045 |
((G \\<turnstile> s1 <=s s1') \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))";
|
|
1046 |
by - (rule wtl_option_pseudo_mono [elimify], simp+);
|
|
1047 |
|
|
1048 |
with a;
|
|
1049 |
show ?thesis;
|
|
1050 |
proof (elim, intro);
|
|
1051 |
fix s1;
|
|
1052 |
assume "G \\<turnstile> s1 <=s s1'" "G \\<turnstile> s1' <=s phi ! Suc pc";
|
|
1053 |
show "G \\<turnstile> s1 <=s phi ! Suc pc"; by (rule sup_state_trans);
|
|
1054 |
qed auto;
|
|
1055 |
qed;
|
|
1056 |
|
|
1057 |
thus ?thesis;
|
|
1058 |
proof (elim exE conjE);
|
|
1059 |
fix s1;
|
|
1060 |
assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc";
|
|
1061 |
assume Gs1: "G \\<turnstile> s1 <=s phi ! Suc pc \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s)";
|
|
1062 |
|
|
1063 |
have "\\<exists>s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)";
|
|
1064 |
proof (cases "G \\<turnstile> s1 <=s phi ! Suc pc");
|
|
1065 |
case True;
|
|
1066 |
with Gs1;
|
|
1067 |
have "G \\<turnstile> s1 <=s phi ! Suc pc"; by simp;
|
|
1068 |
with *;
|
|
1069 |
show ?thesis; by blast;
|
|
1070 |
next;
|
|
1071 |
case False;
|
|
1072 |
with Gs1;
|
|
1073 |
have "\\<exists>c. cert ! Suc pc = Some c \\<and> G \\<turnstile> s1 <=s c"; by simp;
|
|
1074 |
thus ?thesis;
|
|
1075 |
proof elim;
|
|
1076 |
from 1 2 Cons Cons2;
|
|
1077 |
have "Suc pc < length phi"; by (clarsimp_tac simp add: fits_def is_approx_def);
|
|
1078 |
|
|
1079 |
with 1;
|
|
1080 |
have cert: "cert ! (Suc pc) = None \\<or> cert ! (Suc pc) = Some (phi ! Suc pc)";
|
|
1081 |
by (clarsimp_tac simp add: fits_def is_approx_def);
|
|
1082 |
|
|
1083 |
fix c;
|
|
1084 |
assume "cert ! Suc pc = Some c";
|
|
1085 |
with cert;
|
|
1086 |
have c: "c = phi ! Suc pc"; by simp;
|
|
1087 |
assume "G \\<turnstile> s1 <=s c";
|
|
1088 |
with c;
|
|
1089 |
have "G \\<turnstile> s1 <=s phi ! Suc pc"; by simp;
|
|
1090 |
with *;
|
|
1091 |
show ?thesis; by blast;
|
|
1092 |
qed;
|
|
1093 |
qed;
|
|
1094 |
with wto;
|
|
1095 |
show ?thesis; by (auto simp del: split_paired_Ex);
|
|
1096 |
qed;
|
|
1097 |
qed;
|
|
1098 |
qed;
|
|
1099 |
qed;
|
|
1100 |
|
|
1101 |
|
|
1102 |
lemma fits_imp_wtl_method_complete:
|
|
1103 |
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert";
|
|
1104 |
by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
|
|
1105 |
(rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex);
|
|
1106 |
|
|
1107 |
|
|
1108 |
lemma wtl_method_complete:
|
|
1109 |
"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
|
|
1110 |
proof -;
|
|
1111 |
assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
|
|
1112 |
|
|
1113 |
hence "fits ins (make_cert ins phi) phi";
|
|
1114 |
by - (rule fits_make_cert, simp add: wt_method_def);
|
|
1115 |
|
|
1116 |
with *;
|
|
1117 |
show ?thesis; by - (rule fits_imp_wtl_method_complete);
|
|
1118 |
qed;
|
|
1119 |
|
|
1120 |
(*
|
|
1121 |
Goalw[wt_jvm_prog_def, wfprg_def] "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wfprg G";
|
|
1122 |
by Auto_tac;
|
|
1123 |
qed "wt_imp_wfprg";
|
|
1124 |
*)
|
|
1125 |
|
|
1126 |
lemma unique_set:
|
|
1127 |
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
|
|
1128 |
by (induct "l") auto;
|
|
1129 |
|
|
1130 |
lemma unique_epsilon:
|
|
1131 |
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
|
|
1132 |
by (auto simp add: unique_set);
|
|
1133 |
|
|
1134 |
|
|
1135 |
theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
|
|
1136 |
proof (simp only: wt_jvm_prog_def);
|
|
1137 |
|
|
1138 |
assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
|
|
1139 |
|
|
1140 |
thus ?thesis;
|
|
1141 |
proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto);
|
|
1142 |
fix a aa ab b ac ba ad ae bb;
|
|
1143 |
assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
|
|
1144 |
Ball (set fs) (wf_fdecl G) \\<and>
|
|
1145 |
unique fs \\<and>
|
|
1146 |
(\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
|
|
1147 |
unique ms \\<and>
|
|
1148 |
(case sc of None \\<Rightarrow> C = Object
|
|
1149 |
| Some D \\<Rightarrow>
|
|
1150 |
is_class G D \\<and>
|
|
1151 |
(D, C) \\<notin> (subcls1 G)^* \\<and>
|
|
1152 |
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
|
|
1153 |
"(a, aa, ab, b) \\<in> set G";
|
|
1154 |
|
|
1155 |
assume uG : "unique G";
|
|
1156 |
assume b : "((ac, ba), ad, ae, bb) \\<in> set b";
|
|
1157 |
|
|
1158 |
from 1;
|
|
1159 |
show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
|
|
1160 |
proof (rule bspec [elimify], clarsimp_tac);
|
|
1161 |
assume ub : "unique b";
|
|
1162 |
assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb";
|
|
1163 |
from m b;
|
|
1164 |
show ?thesis;
|
|
1165 |
proof (rule bspec [elimify], clarsimp_tac);
|
|
1166 |
assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";
|
|
1167 |
with wfprog uG ub b 1;
|
|
1168 |
show ?thesis;
|
|
1169 |
by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
|
|
1170 |
qed;
|
|
1171 |
qed;
|
|
1172 |
qed;
|
|
1173 |
qed;
|
|
1174 |
|
|
1175 |
end;
|