author | kleing |
Thu, 07 Dec 2000 16:21:47 +0100 | |
changeset 10624 | 850fdf9ce787 |
parent 10612 | 779af7c58743 |
child 10649 | fb27b5547765 |
permissions | -rw-r--r-- |
9580 | 1 |
(* Title: HOL/MicroJava/BV/StepMono.thy |
9559 | 2 |
ID: $Id$ |
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
9594 | 7 |
header {* Monotonicity of step and app *} |
9559 | 8 |
|
9594 | 9 |
theory StepMono = Step: |
9559 | 10 |
|
11 |
||
9580 | 12 |
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)" |
9594 | 13 |
by (auto elim: widen.elims) |
9559 | 14 |
|
15 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
16 |
lemma sup_loc_some [rule_format]: |
10496 | 17 |
"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t --> |
18 |
(\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b") |
|
9664 | 19 |
proof (induct (open) ?P b) |
9559 | 20 |
show "?P []" by simp |
21 |
||
22 |
case Cons |
|
23 |
show "?P (a#list)" |
|
24 |
proof (clarsimp simp add: list_all2_Cons1 sup_loc_def) |
|
25 |
fix z zs n |
|
26 |
assume * : |
|
9580 | 27 |
"G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" |
10496 | 28 |
"n < Suc (length zs)" "(z # zs) ! n = OK t" |
9559 | 29 |
|
10496 | 30 |
show "(\<exists>t. (a # list) ! n = OK t) \<and> G \<turnstile>(a # list) ! n <=o OK t" |
9559 | 31 |
proof (cases n) |
32 |
case 0 |
|
10496 | 33 |
with * show ?thesis by (simp add: sup_ty_opt_OK) |
9559 | 34 |
next |
35 |
case Suc |
|
36 |
with Cons * |
|
37 |
show ?thesis by (simp add: sup_loc_def) |
|
38 |
qed |
|
39 |
qed |
|
40 |
qed |
|
41 |
||
42 |
||
43 |
lemma all_widen_is_sup_loc: |
|
10042 | 44 |
"\<forall>b. length a = length b --> |
10496 | 45 |
(\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))" |
10042 | 46 |
(is "\<forall>b. length a = length b --> ?Q a b" is "?P a") |
9559 | 47 |
proof (induct "a") |
48 |
show "?P []" by simp |
|
49 |
||
50 |
fix l ls assume Cons: "?P ls" |
|
51 |
||
52 |
show "?P (l#ls)" |
|
53 |
proof (intro allI impI) |
|
54 |
fix b |
|
55 |
assume "length (l # ls) = length (b::ty list)" |
|
56 |
with Cons |
|
57 |
show "?Q (l # ls) b" by - (cases b, auto) |
|
58 |
qed |
|
59 |
qed |
|
60 |
||
61 |
||
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
62 |
lemma append_length_n [rule_format]: |
10042 | 63 |
"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x") |
9664 | 64 |
proof (induct (open) ?P x) |
9559 | 65 |
show "?P []" by simp |
66 |
||
67 |
fix l ls assume Cons: "?P ls" |
|
68 |
||
69 |
show "?P (l#ls)" |
|
70 |
proof (intro allI impI) |
|
71 |
fix n |
|
9580 | 72 |
assume l: "n \<le> length (l # ls)" |
9559 | 73 |
|
9580 | 74 |
show "\<exists>a b. l # ls = a @ b \<and> length a = n" |
9559 | 75 |
proof (cases n) |
76 |
assume "n=0" thus ?thesis by simp |
|
77 |
next |
|
78 |
fix "n'" assume s: "n = Suc n'" |
|
79 |
with l |
|
9580 | 80 |
have "n' \<le> length ls" by simp |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
81 |
hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format]) |
9559 | 82 |
thus ?thesis |
83 |
proof elim |
|
84 |
fix a b |
|
85 |
assume "ls = a @ b" "length a = n'" |
|
86 |
with s |
|
9580 | 87 |
have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp |
9559 | 88 |
thus ?thesis by blast |
89 |
qed |
|
90 |
qed |
|
91 |
qed |
|
92 |
qed |
|
93 |
||
94 |
||
95 |
||
96 |
lemma rev_append_cons: |
|
10042 | 97 |
"[|n < length x|] ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n" |
9559 | 98 |
proof - |
99 |
assume n: "n < length x" |
|
9580 | 100 |
hence "n \<le> length x" by simp |
101 |
hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n) |
|
9559 | 102 |
thus ?thesis |
103 |
proof elim |
|
104 |
fix r d assume x: "x = r@d" "length r = n" |
|
105 |
with n |
|
9580 | 106 |
have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv) |
9559 | 107 |
|
108 |
thus ?thesis |
|
109 |
proof elim |
|
110 |
fix b c |
|
111 |
assume "d = b#c" |
|
112 |
with x |
|
9580 | 113 |
have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp |
9559 | 114 |
thus ?thesis by blast |
115 |
qed |
|
116 |
qed |
|
117 |
qed |
|
118 |
||
119 |
||
120 |
lemma app_mono: |
|
10592 | 121 |
"[|G \<turnstile> s <=' s'; app i G m rT s'|] ==> app i G m rT s"; |
9559 | 122 |
proof - |
123 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
124 |
{ fix s1 s2 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
125 |
assume G: "G \<turnstile> s2 <=s s1" |
10592 | 126 |
assume app: "app i G m rT (Some s1)" |
9559 | 127 |
|
10592 | 128 |
from G |
129 |
have l: "length (fst s2) = length (fst s1)" |
|
130 |
by simp |
|
131 |
||
132 |
have "app i G m rT (Some s2)" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
133 |
proof (cases (open) i) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
134 |
case Load |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
135 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
136 |
from G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
137 |
have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
138 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
139 |
from G Load app |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
140 |
have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
141 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
142 |
with G Load app l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
143 |
show ?thesis by clarsimp (drule sup_loc_some, simp+) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
144 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
145 |
case Store |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
146 |
with G app |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
147 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
148 |
by - (cases s2, |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
149 |
auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
150 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
151 |
case Bipush |
10592 | 152 |
with G app |
153 |
show ?thesis by simp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
154 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
155 |
case Aconst_null |
10592 | 156 |
with G app |
157 |
show ?thesis by simp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
158 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
159 |
case New |
10592 | 160 |
with G app |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
161 |
show ?thesis by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
162 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
163 |
case Getfield |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
164 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
165 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
166 |
by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
167 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
168 |
case Putfield |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
169 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
170 |
with app |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
171 |
obtain vT oT ST LT b |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
172 |
where s1: "s1 = (vT # oT # ST, LT)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
173 |
"field (G, cname) vname = Some (cname, b)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
"is_class G cname" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
oT: "G\<turnstile> oT\<preceq> (Class cname)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
176 |
vT: "G\<turnstile> vT\<preceq> b" |
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
177 |
by force |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
179 |
from s1 G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
180 |
obtain vT' oT' ST' LT' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
181 |
where s2: "s2 = (vT' # oT' # ST', LT')" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
182 |
oT': "G\<turnstile> oT' \<preceq> oT" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
183 |
vT': "G\<turnstile> vT' \<preceq> vT" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
184 |
by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
185 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
186 |
from vT' vT |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
188 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
189 |
from oT' oT |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
190 |
have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
191 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
192 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
193 |
by (auto simp add: Putfield) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
194 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
195 |
case Checkcast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
196 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
197 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
198 |
by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
199 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
200 |
case Return |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
201 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
202 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
203 |
by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
204 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
205 |
case Pop |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
206 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
207 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
208 |
by - (cases s2, clarsimp simp add: sup_state_Cons2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
209 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
210 |
case Dup |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
211 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
212 |
show ?thesis |
10592 | 213 |
by - (cases s2, clarsimp simp add: sup_state_Cons2, |
214 |
auto dest: sup_state_length) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
215 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
216 |
case Dup_x1 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
217 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
218 |
show ?thesis |
10592 | 219 |
by - (cases s2, clarsimp simp add: sup_state_Cons2, |
220 |
auto dest: sup_state_length) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
221 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
222 |
case Dup_x2 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
223 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
224 |
show ?thesis |
10592 | 225 |
by - (cases s2, clarsimp simp add: sup_state_Cons2, |
226 |
auto dest: sup_state_length) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
227 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
228 |
case Swap |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
229 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
230 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
231 |
by - (cases s2, clarsimp simp add: sup_state_Cons2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
232 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
233 |
case IAdd |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
234 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
235 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
236 |
by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
237 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
238 |
case Goto |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
239 |
with app |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
240 |
show ?thesis by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
241 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
242 |
case Ifcmpeq |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
243 |
with app G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
244 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
245 |
by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
246 |
next |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
247 |
case Invoke |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
248 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
249 |
with app |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
250 |
obtain apTs X ST LT mD' rT' b' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
251 |
s1: "s1 = (rev apTs @ X # ST, LT)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
252 |
l: "length apTs = length list" and |
10624 | 253 |
c: "is_class G cname" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
254 |
C: "G \<turnstile> X \<preceq> Class cname" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
255 |
w: "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
256 |
m: "method (G, cname) (mname, list) = Some (mD', rT', b')" |
10624 | 257 |
by (simp del: not_None_eq, elim exE conjE) (rule that) |
9559 | 258 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
259 |
obtain apTs' X' ST' LT' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
260 |
s2: "s2 = (rev apTs' @ X' # ST', LT')" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
261 |
l': "length apTs' = length list" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
262 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
263 |
from l s1 G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
264 |
have "length list < length (fst s2)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
265 |
by (simp add: sup_state_length) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
266 |
hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list" |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
267 |
by (rule rev_append_cons [rule_format]) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
268 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
269 |
by - (cases s2, elim exE conjE, simp, rule that) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
270 |
qed |
9559 | 271 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
272 |
from l l' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
273 |
have "length (rev apTs') = length (rev apTs)" by simp |
9559 | 274 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
275 |
from this s1 s2 G |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
276 |
obtain |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
277 |
G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
278 |
X : "G \<turnstile> X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
279 |
by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1) |
9559 | 280 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
281 |
with C |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
282 |
have C': "G \<turnstile> X' \<preceq> Class cname" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
283 |
by - (rule widen_trans, auto) |
9559 | 284 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
285 |
from G' |
10496 | 286 |
have "G \<turnstile> map OK apTs' <=l map OK apTs" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
287 |
by (simp add: sup_state_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
288 |
also |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
289 |
from l w |
10496 | 290 |
have "G \<turnstile> map OK apTs <=l map OK list" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
291 |
by (simp add: all_widen_is_sup_loc) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
292 |
finally |
10496 | 293 |
have "G \<turnstile> map OK apTs' <=l map OK list" . |
9559 | 294 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
295 |
with l' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
296 |
have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
297 |
by (simp add: all_widen_is_sup_loc) |
9559 | 298 |
|
10624 | 299 |
from Invoke s2 l' w' C' m c |
10592 | 300 |
show ?thesis |
301 |
by (simp del: split_paired_Ex) blast |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
302 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
303 |
} note mono_Some = this |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
304 |
|
10592 | 305 |
assume "G \<turnstile> s <=' s'" "app i G m rT s'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
306 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
307 |
thus ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
308 |
by - (cases s, cases s', auto simp add: mono_Some) |
9559 | 309 |
qed |
310 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
311 |
lemmas [simp del] = split_paired_Ex |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
312 |
lemmas [simp] = step_def |
9559 | 313 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
314 |
lemma step_mono_Some: |
10592 | 315 |
"[| app i G m rT (Some s2); G \<turnstile> s1 <=s s2 |] ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
316 |
G \<turnstile> the (step i G (Some s1)) <=s the (step i G (Some s2))" |
9559 | 317 |
proof (cases s1, cases s2) |
318 |
fix a1 b1 a2 b2 |
|
319 |
assume s: "s1 = (a1,b1)" "s2 = (a2,b2)" |
|
10592 | 320 |
assume app2: "app i G m rT (Some s2)" |
9580 | 321 |
assume G: "G \<turnstile> s1 <=s s2" |
9559 | 322 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
323 |
hence "G \<turnstile> Some s1 <=' Some s2" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
324 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
325 |
from this app2 |
10592 | 326 |
have app1: "app i G m rT (Some s1)" by (rule app_mono) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
327 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
328 |
have "step i G (Some s1) \<noteq> None \<and> step i G (Some s2) \<noteq> None" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
329 |
by simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
330 |
then |
9559 | 331 |
obtain a1' b1' a2' b2' |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
332 |
where step: "step i G (Some s1) = Some (a1',b1')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
333 |
"step i G (Some s2) = Some (a2',b2')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
334 |
by (auto simp del: step_def simp add: s) |
9559 | 335 |
|
9580 | 336 |
have "G \<turnstile> (a1',b1') <=s (a2',b2')" |
9664 | 337 |
proof (cases (open) i) |
9559 | 338 |
case Load |
339 |
||
340 |
with s app1 |
|
341 |
obtain y where |
|
10496 | 342 |
y: "nat < length b1" "b1 ! nat = OK y" by clarsimp |
9559 | 343 |
|
344 |
from Load s app2 |
|
345 |
obtain y' where |
|
10496 | 346 |
y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp |
9559 | 347 |
|
348 |
from G s |
|
9580 | 349 |
have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def) |
9559 | 350 |
|
351 |
with y y' |
|
9580 | 352 |
have "G \<turnstile> y \<preceq> y'" |
9559 | 353 |
by - (drule sup_loc_some, simp+) |
354 |
||
355 |
with Load G y y' s step app1 app2 |
|
356 |
show ?thesis by (clarsimp simp add: sup_state_def) |
|
357 |
next |
|
358 |
case Store |
|
359 |
with G s step app1 app2 |
|
360 |
show ?thesis |
|
361 |
by (clarsimp simp add: sup_state_def sup_loc_update) |
|
362 |
next |
|
363 |
case Bipush |
|
364 |
with G s step app1 app2 |
|
365 |
show ?thesis |
|
366 |
by (clarsimp simp add: sup_state_Cons1) |
|
367 |
next |
|
368 |
case New |
|
369 |
with G s step app1 app2 |
|
370 |
show ?thesis |
|
371 |
by (clarsimp simp add: sup_state_Cons1) |
|
372 |
next |
|
373 |
case Aconst_null |
|
374 |
with G s step app1 app2 |
|
375 |
show ?thesis |
|
376 |
by (clarsimp simp add: sup_state_Cons1) |
|
377 |
next |
|
378 |
case Getfield |
|
379 |
with G s step app1 app2 |
|
380 |
show ?thesis |
|
381 |
by (clarsimp simp add: sup_state_Cons1) |
|
382 |
next |
|
383 |
case Putfield |
|
384 |
with G s step app1 app2 |
|
385 |
show ?thesis |
|
386 |
by (clarsimp simp add: sup_state_Cons1) |
|
387 |
next |
|
388 |
case Checkcast |
|
389 |
with G s step app1 app2 |
|
390 |
show ?thesis |
|
391 |
by (clarsimp simp add: sup_state_Cons1) |
|
392 |
next |
|
393 |
case Invoke |
|
394 |
||
395 |
with s app1 |
|
396 |
obtain a X ST where |
|
397 |
s1: "s1 = (a @ X # ST, b1)" and |
|
398 |
l: "length a = length list" |
|
399 |
by (simp, elim exE conjE, simp) |
|
400 |
||
401 |
from Invoke s app2 |
|
402 |
obtain a' X' ST' where |
|
403 |
s2: "s2 = (a' @ X' # ST', b2)" and |
|
404 |
l': "length a' = length list" |
|
405 |
by (simp, elim exE conjE, simp) |
|
406 |
||
407 |
from l l' |
|
408 |
have lr: "length a = length a'" by simp |
|
409 |
||
410 |
from lr G s s1 s2 |
|
9580 | 411 |
have "G \<turnstile> (ST, b1) <=s (ST', b2)" |
9559 | 412 |
by (simp add: sup_state_append_fst sup_state_Cons1) |
413 |
||
414 |
moreover |
|
415 |
||
416 |
from Invoke G s step app1 app2 |
|
9580 | 417 |
have "b1 = b1' \<and> b2 = b2'" by simp |
9559 | 418 |
|
419 |
ultimately |
|
420 |
||
9580 | 421 |
have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp |
9559 | 422 |
|
423 |
with Invoke G s step app1 app2 s1 s2 l l' |
|
424 |
show ?thesis |
|
425 |
by (clarsimp simp add: sup_state_def) |
|
426 |
next |
|
10496 | 427 |
case Return |
428 |
with G step |
|
429 |
show ?thesis |
|
430 |
by simp |
|
9559 | 431 |
next |
432 |
case Pop |
|
433 |
with G s step app1 app2 |
|
434 |
show ?thesis |
|
435 |
by (clarsimp simp add: sup_state_Cons1) |
|
436 |
next |
|
437 |
case Dup |
|
438 |
with G s step app1 app2 |
|
439 |
show ?thesis |
|
440 |
by (clarsimp simp add: sup_state_Cons1) |
|
441 |
next |
|
442 |
case Dup_x1 |
|
443 |
with G s step app1 app2 |
|
444 |
show ?thesis |
|
445 |
by (clarsimp simp add: sup_state_Cons1) |
|
446 |
next |
|
447 |
case Dup_x2 |
|
448 |
with G s step app1 app2 |
|
449 |
show ?thesis |
|
450 |
by (clarsimp simp add: sup_state_Cons1) |
|
451 |
next |
|
452 |
case Swap |
|
453 |
with G s step app1 app2 |
|
454 |
show ?thesis |
|
455 |
by (clarsimp simp add: sup_state_Cons1) |
|
456 |
next |
|
457 |
case IAdd |
|
458 |
with G s step app1 app2 |
|
459 |
show ?thesis |
|
460 |
by (clarsimp simp add: sup_state_Cons1) |
|
461 |
next |
|
462 |
case Goto |
|
463 |
with G s step app1 app2 |
|
464 |
show ?thesis by simp |
|
465 |
next |
|
466 |
case Ifcmpeq |
|
467 |
with G s step app1 app2 |
|
468 |
show ?thesis |
|
469 |
by (clarsimp simp add: sup_state_Cons1) |
|
470 |
qed |
|
471 |
||
472 |
with step |
|
473 |
show ?thesis by auto |
|
474 |
qed |
|
475 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
476 |
lemma step_mono: |
10592 | 477 |
"[| app i G m rT s2; G \<turnstile> s1 <=' s2 |] ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
478 |
G \<turnstile> step i G s1 <=' step i G s2" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
479 |
by (cases s1, cases s2, auto dest: step_mono_Some) |
9559 | 480 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
481 |
lemmas [simp del] = step_def |
9559 | 482 |
|
483 |
end |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
484 |