1 (* Title: HOL/MicroJava/BV/Convert.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch and Gerwin Klein |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 header "Lifted Type Relations" |
|
8 |
|
9 theory Convert = Err + JVMExec: |
|
10 |
|
11 text "The supertype relation lifted to type err, type lists and state types." |
|
12 |
|
13 types |
|
14 locvars_type = "ty err list" |
|
15 opstack_type = "ty list" |
|
16 state_type = "opstack_type \<times> locvars_type" |
|
17 method_type = "state_type option list" |
|
18 class_type = "sig => method_type" |
|
19 prog_type = "cname => class_type" |
|
20 |
|
21 consts |
|
22 strict :: "('a => 'b err) => ('a err => 'b err)" |
|
23 primrec |
|
24 "strict f Err = Err" |
|
25 "strict f (OK x) = f x" |
|
26 |
|
27 |
|
28 constdefs |
|
29 (* lifts a relation to err with Err as top element *) |
|
30 lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)" |
|
31 "lift_top P a' a == case a of |
|
32 Err => True |
|
33 | OK t => (case a' of Err => False | OK t' => P t' t)" |
|
34 |
|
35 (* lifts a relation to option with None as bottom element *) |
|
36 lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)" |
|
37 "lift_bottom P a' a == |
|
38 case a' of |
|
39 None => True |
|
40 | Some t' => (case a of None => False | Some t => P t' t)" |
|
41 |
|
42 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
|
43 ("_ \<turnstile> _ <=o _" [71,71] 70) |
|
44 "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')" |
|
45 |
|
46 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
|
47 ("_ \<turnstile> _ <=l _" [71,71] 70) |
|
48 "G \<turnstile> LT <=l LT' == list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'" |
|
49 |
|
50 sup_state :: "['code prog,state_type,state_type] => bool" |
|
51 ("_ \<turnstile> _ <=s _" [71,71] 70) |
|
52 "G \<turnstile> s <=s s' == |
|
53 (G \<turnstile> map OK (fst s) <=l map OK (fst s')) \<and> G \<turnstile> snd s <=l snd s'" |
|
54 |
|
55 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
|
56 ("_ \<turnstile> _ <=' _" [71,71] 70) |
|
57 "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')" |
|
58 |
|
59 syntax (HTML) |
|
60 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
|
61 ("_ |- _ <=o _") |
|
62 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
|
63 ("_ |- _ <=l _" [71,71] 70) |
|
64 sup_state :: "['code prog,state_type,state_type] => bool" |
|
65 ("_ |- _ <=s _" [71,71] 70) |
|
66 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
|
67 ("_ |- _ <=' _" [71,71] 70) |
|
68 |
|
69 |
|
70 lemmas [iff] = not_Err_eq not_OK_eq |
|
71 |
|
72 lemma lift_top_refl [simp]: |
|
73 "[| !!x. P x x |] ==> lift_top P x x" |
|
74 by (simp add: lift_top_def split: err.splits) |
|
75 |
|
76 lemma lift_top_trans [trans]: |
|
77 "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] |
|
78 ==> lift_top P x z" |
|
79 proof - |
|
80 assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" |
|
81 assume a: "lift_top P x y" |
|
82 assume b: "lift_top P y z" |
|
83 |
|
84 { assume "z = Err" |
|
85 hence ?thesis by (simp add: lift_top_def) |
|
86 } note z_none = this |
|
87 |
|
88 { assume "x = Err" |
|
89 with a b |
|
90 have ?thesis |
|
91 by (simp add: lift_top_def split: err.splits) |
|
92 } note x_none = this |
|
93 |
|
94 { fix r t |
|
95 assume x: "x = OK r" and z: "z = OK t" |
|
96 with a b |
|
97 obtain s where y: "y = OK s" |
|
98 by (simp add: lift_top_def split: err.splits) |
|
99 |
|
100 from a x y |
|
101 have "P r s" by (simp add: lift_top_def) |
|
102 also |
|
103 from b y z |
|
104 have "P s t" by (simp add: lift_top_def) |
|
105 finally |
|
106 have "P r t" . |
|
107 |
|
108 with x z |
|
109 have ?thesis by (simp add: lift_top_def) |
|
110 } |
|
111 |
|
112 with x_none z_none |
|
113 show ?thesis by blast |
|
114 qed |
|
115 |
|
116 lemma lift_top_Err_any [simp]: |
|
117 "lift_top P Err any = (any = Err)" |
|
118 by (simp add: lift_top_def split: err.splits) |
|
119 |
|
120 lemma lift_top_OK_OK [simp]: |
|
121 "lift_top P (OK a) (OK b) = P a b" |
|
122 by (simp add: lift_top_def split: err.splits) |
|
123 |
|
124 lemma lift_top_any_OK [simp]: |
|
125 "lift_top P any (OK b) = (\<exists>a. any = OK a \<and> P a b)" |
|
126 by (simp add: lift_top_def split: err.splits) |
|
127 |
|
128 lemma lift_top_OK_any: |
|
129 "lift_top P (OK a) any = (any = Err \<or> (\<exists>b. any = OK b \<and> P a b))" |
|
130 by (simp add: lift_top_def split: err.splits) |
|
131 |
|
132 |
|
133 lemma lift_bottom_refl [simp]: |
|
134 "[| !!x. P x x |] ==> lift_bottom P x x" |
|
135 by (simp add: lift_bottom_def split: option.splits) |
|
136 |
|
137 lemma lift_bottom_trans [trans]: |
|
138 "[| !!x y z. [| P x y; P y z |] ==> P x z; |
|
139 lift_bottom P x y; lift_bottom P y z |] |
|
140 ==> lift_bottom P x z" |
|
141 proof - |
|
142 assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" |
|
143 assume a: "lift_bottom P x y" |
|
144 assume b: "lift_bottom P y z" |
|
145 |
|
146 { assume "x = None" |
|
147 hence ?thesis by (simp add: lift_bottom_def) |
|
148 } note z_none = this |
|
149 |
|
150 { assume "z = None" |
|
151 with a b |
|
152 have ?thesis |
|
153 by (simp add: lift_bottom_def split: option.splits) |
|
154 } note x_none = this |
|
155 |
|
156 { fix r t |
|
157 assume x: "x = Some r" and z: "z = Some t" |
|
158 with a b |
|
159 obtain s where y: "y = Some s" |
|
160 by (simp add: lift_bottom_def split: option.splits) |
|
161 |
|
162 from a x y |
|
163 have "P r s" by (simp add: lift_bottom_def) |
|
164 also |
|
165 from b y z |
|
166 have "P s t" by (simp add: lift_bottom_def) |
|
167 finally |
|
168 have "P r t" . |
|
169 |
|
170 with x z |
|
171 have ?thesis by (simp add: lift_bottom_def) |
|
172 } |
|
173 |
|
174 with x_none z_none |
|
175 show ?thesis by blast |
|
176 qed |
|
177 |
|
178 lemma lift_bottom_any_None [simp]: |
|
179 "lift_bottom P any None = (any = None)" |
|
180 by (simp add: lift_bottom_def split: option.splits) |
|
181 |
|
182 lemma lift_bottom_Some_Some [simp]: |
|
183 "lift_bottom P (Some a) (Some b) = P a b" |
|
184 by (simp add: lift_bottom_def split: option.splits) |
|
185 |
|
186 lemma lift_bottom_any_Some [simp]: |
|
187 "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)" |
|
188 by (simp add: lift_bottom_def split: option.splits) |
|
189 |
|
190 lemma lift_bottom_Some_any: |
|
191 "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))" |
|
192 by (simp add: lift_bottom_def split: option.splits) |
|
193 |
|
194 |
|
195 |
|
196 theorem sup_ty_opt_refl [simp]: |
|
197 "G \<turnstile> t <=o t" |
|
198 by (simp add: sup_ty_opt_def) |
|
199 |
|
200 theorem sup_loc_refl [simp]: |
|
201 "G \<turnstile> t <=l t" |
|
202 by (induct t, auto simp add: sup_loc_def) |
|
203 |
|
204 theorem sup_state_refl [simp]: |
|
205 "G \<turnstile> s <=s s" |
|
206 by (simp add: sup_state_def) |
|
207 |
|
208 theorem sup_state_opt_refl [simp]: |
|
209 "G \<turnstile> s <=' s" |
|
210 by (simp add: sup_state_opt_def) |
|
211 |
|
212 |
|
213 theorem anyConvErr [simp]: |
|
214 "(G \<turnstile> Err <=o any) = (any = Err)" |
|
215 by (simp add: sup_ty_opt_def) |
|
216 |
|
217 theorem OKanyConvOK [simp]: |
|
218 "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)" |
|
219 by (simp add: sup_ty_opt_def) |
|
220 |
|
221 theorem sup_ty_opt_OK: |
|
222 "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x" |
|
223 by (clarsimp simp add: sup_ty_opt_def) |
|
224 |
|
225 lemma widen_PrimT_conv1 [simp]: |
|
226 "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x" |
|
227 by (auto elim: widen.elims) |
|
228 |
|
229 theorem sup_PTS_eq: |
|
230 "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))" |
|
231 by (auto simp add: sup_ty_opt_def lift_top_OK_any) |
|
232 |
|
233 |
|
234 |
|
235 theorem sup_loc_Nil [iff]: |
|
236 "(G \<turnstile> [] <=l XT) = (XT=[])" |
|
237 by (simp add: sup_loc_def) |
|
238 |
|
239 theorem sup_loc_Cons [iff]: |
|
240 "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))" |
|
241 by (simp add: sup_loc_def list_all2_Cons1) |
|
242 |
|
243 theorem sup_loc_Cons2: |
|
244 "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))" |
|
245 by (simp add: sup_loc_def list_all2_Cons2) |
|
246 |
|
247 |
|
248 theorem sup_loc_length: |
|
249 "G \<turnstile> a <=l b ==> length a = length b" |
|
250 proof - |
|
251 assume G: "G \<turnstile> a <=l b" |
|
252 have "\<forall> b. (G \<turnstile> a <=l b) --> length a = length b" |
|
253 by (induct a, auto) |
|
254 with G |
|
255 show ?thesis by blast |
|
256 qed |
|
257 |
|
258 theorem sup_loc_nth: |
|
259 "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)" |
|
260 proof - |
|
261 assume a: "G \<turnstile> a <=l b" "n < length a" |
|
262 have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))" |
|
263 (is "?P a") |
|
264 proof (induct a) |
|
265 show "?P []" by simp |
|
266 |
|
267 fix x xs assume IH: "?P xs" |
|
268 |
|
269 show "?P (x#xs)" |
|
270 proof (intro strip) |
|
271 fix n b |
|
272 assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)" |
|
273 with IH |
|
274 show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)" |
|
275 by - (cases n, auto) |
|
276 qed |
|
277 qed |
|
278 with a |
|
279 show ?thesis by blast |
|
280 qed |
|
281 |
|
282 |
|
283 theorem all_nth_sup_loc: |
|
284 "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) |
|
285 --> (G \<turnstile> a <=l b)" (is "?P a") |
|
286 proof (induct a) |
|
287 show "?P []" by simp |
|
288 |
|
289 fix l ls assume IH: "?P ls" |
|
290 |
|
291 show "?P (l#ls)" |
|
292 proof (intro strip) |
|
293 fix b |
|
294 assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))" |
|
295 assume l: "length (l#ls) = length b" |
|
296 |
|
297 then obtain b' bs where b: "b = b'#bs" |
|
298 by - (cases b, simp, simp add: neq_Nil_conv, rule that) |
|
299 |
|
300 with f |
|
301 have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))" |
|
302 by auto |
|
303 |
|
304 with f b l IH |
|
305 show "G \<turnstile> (l # ls) <=l b" |
|
306 by auto |
|
307 qed |
|
308 qed |
|
309 |
|
310 |
|
311 theorem sup_loc_append: |
|
312 "length a = length b ==> |
|
313 (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))" |
|
314 proof - |
|
315 assume l: "length a = length b" |
|
316 |
|
317 have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> |
|
318 (G \<turnstile> x <=l y))" (is "?P a") |
|
319 proof (induct a) |
|
320 show "?P []" by simp |
|
321 |
|
322 fix l ls assume IH: "?P ls" |
|
323 show "?P (l#ls)" |
|
324 proof (intro strip) |
|
325 fix b |
|
326 assume "length (l#ls) = length (b::ty err list)" |
|
327 with IH |
|
328 show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))" |
|
329 by - (cases b, auto) |
|
330 qed |
|
331 qed |
|
332 with l |
|
333 show ?thesis by blast |
|
334 qed |
|
335 |
|
336 theorem sup_loc_rev [simp]: |
|
337 "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" |
|
338 proof - |
|
339 have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a") |
|
340 proof (induct a) |
|
341 show "?P []" by simp |
|
342 |
|
343 fix l ls assume IH: "?P ls" |
|
344 |
|
345 { |
|
346 fix b |
|
347 have "?Q (l#ls) b" |
|
348 proof (cases (open) b) |
|
349 case Nil |
|
350 thus ?thesis by (auto dest: sup_loc_length) |
|
351 next |
|
352 case Cons |
|
353 show ?thesis |
|
354 proof |
|
355 assume "G \<turnstile> (l # ls) <=l b" |
|
356 thus "G \<turnstile> rev (l # ls) <=l rev b" |
|
357 by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append) |
|
358 next |
|
359 assume "G \<turnstile> rev (l # ls) <=l rev b" |
|
360 hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])" |
|
361 by (simp add: Cons) |
|
362 |
|
363 hence "length (rev ls) = length (rev list)" |
|
364 by (auto dest: sup_loc_length) |
|
365 |
|
366 from this G |
|
367 obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a" |
|
368 by (simp add: sup_loc_append) |
|
369 |
|
370 thus "G \<turnstile> (l # ls) <=l b" |
|
371 by (simp add: Cons IH) |
|
372 qed |
|
373 qed |
|
374 } |
|
375 thus "?P (l#ls)" by blast |
|
376 qed |
|
377 |
|
378 thus ?thesis by blast |
|
379 qed |
|
380 |
|
381 |
|
382 theorem sup_loc_update [rule_format]: |
|
383 "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> |
|
384 (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x") |
|
385 proof (induct x) |
|
386 show "?P []" by simp |
|
387 |
|
388 fix l ls assume IH: "?P ls" |
|
389 show "?P (l#ls)" |
|
390 proof (intro strip) |
|
391 fix n y |
|
392 assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y" |
|
393 with IH |
|
394 show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]" |
|
395 by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1) |
|
396 qed |
|
397 qed |
|
398 |
|
399 |
|
400 theorem sup_state_length [simp]: |
|
401 "G \<turnstile> s2 <=s s1 ==> |
|
402 length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)" |
|
403 by (auto dest: sup_loc_length simp add: sup_state_def); |
|
404 |
|
405 theorem sup_state_append_snd: |
|
406 "length a = length b ==> |
|
407 (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))" |
|
408 by (auto simp add: sup_state_def sup_loc_append) |
|
409 |
|
410 theorem sup_state_append_fst: |
|
411 "length a = length b ==> |
|
412 (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))" |
|
413 by (auto simp add: sup_state_def sup_loc_append) |
|
414 |
|
415 theorem sup_state_Cons1: |
|
416 "(G \<turnstile> (x#xt, a) <=s (yt, b)) = |
|
417 (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))" |
|
418 by (auto simp add: sup_state_def map_eq_Cons) |
|
419 |
|
420 theorem sup_state_Cons2: |
|
421 "(G \<turnstile> (xt, a) <=s (y#yt, b)) = |
|
422 (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))" |
|
423 by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2) |
|
424 |
|
425 theorem sup_state_ignore_fst: |
|
426 "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)" |
|
427 by (simp add: sup_state_def) |
|
428 |
|
429 theorem sup_state_rev_fst: |
|
430 "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))" |
|
431 proof - |
|
432 have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map) |
|
433 show ?thesis by (simp add: m sup_state_def) |
|
434 qed |
|
435 |
|
436 |
|
437 lemma sup_state_opt_None_any [iff]: |
|
438 "(G \<turnstile> None <=' any) = True" |
|
439 by (simp add: sup_state_opt_def lift_bottom_def) |
|
440 |
|
441 lemma sup_state_opt_any_None [iff]: |
|
442 "(G \<turnstile> any <=' None) = (any = None)" |
|
443 by (simp add: sup_state_opt_def) |
|
444 |
|
445 lemma sup_state_opt_Some_Some [iff]: |
|
446 "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)" |
|
447 by (simp add: sup_state_opt_def del: split_paired_Ex) |
|
448 |
|
449 lemma sup_state_opt_any_Some [iff]: |
|
450 "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)" |
|
451 by (simp add: sup_state_opt_def) |
|
452 |
|
453 lemma sup_state_opt_Some_any: |
|
454 "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))" |
|
455 by (simp add: sup_state_opt_def lift_bottom_Some_any) |
|
456 |
|
457 |
|
458 theorem sup_ty_opt_trans [trans]: |
|
459 "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c" |
|
460 by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def) |
|
461 |
|
462 theorem sup_loc_trans [trans]: |
|
463 "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c" |
|
464 proof - |
|
465 assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c" |
|
466 |
|
467 hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))" |
|
468 proof (intro strip) |
|
469 fix n |
|
470 assume n: "n < length a" |
|
471 with G |
|
472 have "G \<turnstile> (a!n) <=o (b!n)" |
|
473 by - (rule sup_loc_nth) |
|
474 also |
|
475 from n G |
|
476 have "G \<turnstile> ... <=o (c!n)" |
|
477 by - (rule sup_loc_nth, auto dest: sup_loc_length) |
|
478 finally |
|
479 show "G \<turnstile> (a!n) <=o (c!n)" . |
|
480 qed |
|
481 |
|
482 with G |
|
483 show ?thesis |
|
484 by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) |
|
485 qed |
|
486 |
|
487 |
|
488 theorem sup_state_trans [trans]: |
|
489 "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c" |
|
490 by (auto intro: sup_loc_trans simp add: sup_state_def) |
|
491 |
|
492 theorem sup_state_opt_trans [trans]: |
|
493 "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c" |
|
494 by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def) |
|
495 |
|
496 |
|
497 end |
|