|
1 theory Comp_Rev |
|
2 imports Compiler |
|
3 begin |
|
4 |
|
5 section {* Compiler Correctness, 2nd direction *} |
|
6 |
|
7 subsection {* Definitions *} |
|
8 |
|
9 text {* Execution in @{term n} steps for simpler induction *} |
|
10 primrec |
|
11 exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" |
|
12 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55) |
|
13 where |
|
14 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
|
15 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
|
16 |
|
17 text {* The possible successor pc's of an instruction at position @{term n} *} |
|
18 definition |
|
19 "isuccs i n \<equiv> case i of |
|
20 JMP j \<Rightarrow> {n + 1 + j} |
|
21 | JMPFLESS j \<Rightarrow> {n + 1 + j, n + 1} |
|
22 | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1} |
|
23 | _ \<Rightarrow> {n +1}" |
|
24 |
|
25 (* FIXME: _Collect? *) |
|
26 text {* The possible successors pc's of an instruction list *} |
|
27 definition |
|
28 "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}" |
|
29 |
|
30 text {* Possible exit pc's of a program *} |
|
31 definition |
|
32 "exits P = succs P 0 - {0..< isize P}" |
|
33 |
|
34 |
|
35 subsection {* Basic properties of @{term exec_n} *} |
|
36 |
|
37 lemma exec_n_exec: |
|
38 "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'" |
|
39 by (induct n arbitrary: c) (auto intro: exec.step) |
|
40 |
|
41 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp |
|
42 |
|
43 lemma exec_Suc [trans]: |
|
44 "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''" |
|
45 by (fastsimp simp del: split_paired_Ex) |
|
46 |
|
47 lemma exec_exec_n: |
|
48 "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'" |
|
49 by (induct rule: exec.induct) (auto intro: exec_Suc) |
|
50 |
|
51 lemma exec_eq_exec_n: |
|
52 "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')" |
|
53 by (blast intro: exec_exec_n exec_n_exec) |
|
54 |
|
55 lemma exec_n_Nil [simp]: |
|
56 "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)" |
|
57 by (induct k) auto |
|
58 |
|
59 lemma exec1_exec_n [elim,intro!]: |
|
60 "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'" |
|
61 by (cases c') simp |
|
62 |
|
63 |
|
64 subsection {* Concrete symbolic execution steps *} |
|
65 |
|
66 lemma exec_n_step: |
|
67 "n \<noteq> n' \<Longrightarrow> |
|
68 P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') = |
|
69 (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)" |
|
70 by (cases k) auto |
|
71 |
|
72 lemma exec1_end: |
|
73 "isize P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'" |
|
74 by auto |
|
75 |
|
76 lemma exec_n_end: |
|
77 "isize P <= n \<Longrightarrow> |
|
78 P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)" |
|
79 by (cases k) (auto simp: exec1_end) |
|
80 |
|
81 lemmas exec_n_simps = exec_n_step exec_n_end |
|
82 |
|
83 |
|
84 subsection {* Basic properties of @{term succs} *} |
|
85 |
|
86 lemma succs_simps [simp]: |
|
87 "succs [ADD] n = {n + 1}" |
|
88 "succs [LOADI v] n = {n + 1}" |
|
89 "succs [LOAD x] n = {n + 1}" |
|
90 "succs [STORE x] n = {n + 1}" |
|
91 "succs [JMP i] n = {n + 1 + i}" |
|
92 "succs [JMPFGE i] n = {n + 1 + i, n + 1}" |
|
93 "succs [JMPFLESS i] n = {n + 1 + i, n + 1}" |
|
94 by (auto simp: succs_def isuccs_def) |
|
95 |
|
96 lemma succs_empty [iff]: "succs [] n = {}" |
|
97 by (simp add: succs_def) |
|
98 |
|
99 lemma succs_Cons: |
|
100 "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs") |
|
101 proof |
|
102 let ?isuccs = "\<lambda>p P n i. 0 \<le> i \<and> i < isize P \<and> p \<in> isuccs (P!!i) (n+i)" |
|
103 { fix p assume "p \<in> succs (x#xs) n" |
|
104 then obtain i where isuccs: "?isuccs p (x#xs) n i" |
|
105 unfolding succs_def by auto |
|
106 have "p \<in> ?x \<union> ?xs" |
|
107 proof cases |
|
108 assume "i = 0" with isuccs show ?thesis by simp |
|
109 next |
|
110 assume "i \<noteq> 0" |
|
111 with isuccs |
|
112 have "?isuccs p xs (1+n) (i - 1)" by auto |
|
113 hence "p \<in> ?xs" unfolding succs_def by blast |
|
114 thus ?thesis .. |
|
115 qed |
|
116 } |
|
117 thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" .. |
|
118 |
|
119 { fix p assume "p \<in> ?x \<or> p \<in> ?xs" |
|
120 hence "p \<in> succs (x#xs) n" |
|
121 proof |
|
122 assume "p \<in> ?x" thus ?thesis by (fastsimp simp: succs_def) |
|
123 next |
|
124 assume "p \<in> ?xs" |
|
125 then obtain i where "?isuccs p xs (1+n) i" |
|
126 unfolding succs_def by auto |
|
127 hence "?isuccs p (x#xs) n (1+i)" |
|
128 by (simp add: algebra_simps) |
|
129 thus ?thesis unfolding succs_def by blast |
|
130 qed |
|
131 } |
|
132 thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast |
|
133 qed |
|
134 |
|
135 lemma succs_iexec1: |
|
136 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> fst c' \<in> succs P 0" |
|
137 by (auto elim!: iexec1.cases simp: succs_def isuccs_def) |
|
138 |
|
139 lemma succs_shift: |
|
140 "(p - n \<in> succs P 0) = (p \<in> succs P n)" |
|
141 by (fastsimp simp: succs_def isuccs_def split: instr.split) |
|
142 |
|
143 lemma inj_op_plus [simp]: |
|
144 "inj (op + (i::int))" |
|
145 by (metis add_minus_cancel inj_on_inverseI) |
|
146 |
|
147 lemma succs_set_shift [simp]: |
|
148 "op + i ` succs xs 0 = succs xs i" |
|
149 by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI) |
|
150 |
|
151 lemma succs_append [simp]: |
|
152 "succs (xs @ ys) n = succs xs n \<union> succs ys (n + isize xs)" |
|
153 by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps) |
|
154 |
|
155 |
|
156 lemma exits_append [simp]: |
|
157 "exits (xs @ ys) = exits xs \<union> (op + (isize xs)) ` exits ys - |
|
158 {0..<isize xs + isize ys}" |
|
159 by (auto simp: exits_def image_set_diff) |
|
160 |
|
161 lemma exits_single: |
|
162 "exits [x] = isuccs x 0 - {0}" |
|
163 by (auto simp: exits_def succs_def) |
|
164 |
|
165 lemma exits_Cons: |
|
166 "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - |
|
167 {0..<1 + isize xs}" |
|
168 using exits_append [of "[x]" xs] |
|
169 by (simp add: exits_single) |
|
170 |
|
171 lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def) |
|
172 |
|
173 lemma exits_simps [simp]: |
|
174 "exits [ADD] = {1}" |
|
175 "exits [LOADI v] = {1}" |
|
176 "exits [LOAD x] = {1}" |
|
177 "exits [STORE x] = {1}" |
|
178 "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}" |
|
179 "i \<noteq> -1 \<Longrightarrow> exits [JMPFGE i] = {1 + i, 1}" |
|
180 "i \<noteq> -1 \<Longrightarrow> exits [JMPFLESS i] = {1 + i, 1}" |
|
181 by (auto simp: exits_def) |
|
182 |
|
183 lemma acomp_succs [simp]: |
|
184 "succs (acomp a) n = {n + 1 .. n + isize (acomp a)}" |
|
185 by (induct a arbitrary: n) auto |
|
186 |
|
187 lemma acomp_size: |
|
188 "1 \<le> isize (acomp a)" |
|
189 by (induct a) auto |
|
190 |
|
191 lemma exits_acomp [simp]: |
|
192 "exits (acomp a) = {isize (acomp a)}" |
|
193 by (auto simp: exits_def acomp_size) |
|
194 |
|
195 lemma bcomp_succs: |
|
196 "0 \<le> i \<Longrightarrow> |
|
197 succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)} |
|
198 \<union> {n + i + isize (bcomp b c i)}" |
|
199 proof (induct b arbitrary: c i n) |
|
200 case (And b1 b2) |
|
201 from And.prems |
|
202 show ?case |
|
203 by (cases c) |
|
204 (auto dest: And.hyps(1) [THEN subsetD, rotated] |
|
205 And.hyps(2) [THEN subsetD, rotated]) |
|
206 qed auto |
|
207 |
|
208 lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated] |
|
209 |
|
210 lemma bcomp_exits: |
|
211 "0 \<le> i \<Longrightarrow> |
|
212 exits (bcomp b c i) \<subseteq> {isize (bcomp b c i), i + isize (bcomp b c i)}" |
|
213 by (auto simp: exits_def) |
|
214 |
|
215 lemma bcomp_exitsD [dest!]: |
|
216 "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow> |
|
217 p = isize (bcomp b c i) \<or> p = i + isize (bcomp b c i)" |
|
218 using bcomp_exits by auto |
|
219 |
|
220 lemma ccomp_succs: |
|
221 "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}" |
|
222 proof (induct c arbitrary: n) |
|
223 case SKIP thus ?case by simp |
|
224 next |
|
225 case Assign thus ?case by simp |
|
226 next |
|
227 case (Semi c1 c2) |
|
228 from Semi.prems |
|
229 show ?case |
|
230 by (fastsimp dest: Semi.hyps [THEN subsetD]) |
|
231 next |
|
232 case (If b c1 c2) |
|
233 from If.prems |
|
234 show ?case |
|
235 by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons) |
|
236 next |
|
237 case (While b c) |
|
238 from While.prems |
|
239 show ?case by (auto dest!: While.hyps [THEN subsetD]) |
|
240 qed |
|
241 |
|
242 lemma ccomp_exits: |
|
243 "exits (ccomp c) \<subseteq> {isize (ccomp c)}" |
|
244 using ccomp_succs [of c 0] by (auto simp: exits_def) |
|
245 |
|
246 lemma ccomp_exitsD [dest!]: |
|
247 "p \<in> exits (ccomp c) \<Longrightarrow> p = isize (ccomp c)" |
|
248 using ccomp_exits by auto |
|
249 |
|
250 |
|
251 subsection {* Splitting up machine executions *} |
|
252 |
|
253 lemma exec1_split: |
|
254 "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize c \<Longrightarrow> |
|
255 c \<turnstile> (i,s) \<rightarrow> (j - isize P, s')" |
|
256 by (auto elim!: iexec1.cases) |
|
257 |
|
258 lemma exec_n_split: |
|
259 shows "\<lbrakk> P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s'); |
|
260 0 \<le> i; i < isize c; j \<notin> {isize P ..< isize P + isize c} \<rbrakk> \<Longrightarrow> |
|
261 \<exists>s'' i' k m. |
|
262 c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and> |
|
263 i' \<in> exits c \<and> |
|
264 P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and> |
|
265 n = k + m" |
|
266 proof (induct n arbitrary: i j s) |
|
267 case 0 |
|
268 thus ?case by simp |
|
269 next |
|
270 case (Suc n) |
|
271 have i: "0 \<le> i" "i < isize c" by fact+ |
|
272 from Suc.prems |
|
273 have j: "\<not> (isize P \<le> j \<and> j < isize P + isize c)" by simp |
|
274 from Suc.prems |
|
275 obtain i0 s0 where |
|
276 step: "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (i0,s0)" and |
|
277 rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')" |
|
278 by clarsimp |
|
279 |
|
280 from step i |
|
281 have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - isize P, s0)" by (rule exec1_split) |
|
282 |
|
283 have "i0 = isize P + (i0 - isize P) " by simp |
|
284 then obtain j0 where j0: "i0 = isize P + j0" .. |
|
285 |
|
286 note split_paired_Ex [simp del] |
|
287 |
|
288 { assume "j0 \<in> {0 ..< isize c}" |
|
289 with j0 j rest c |
|
290 have ?case |
|
291 by (fastsimp dest!: Suc.hyps intro!: exec_Suc) |
|
292 } moreover { |
|
293 assume "j0 \<notin> {0 ..< isize c}" |
|
294 moreover |
|
295 from c j0 have "j0 \<in> succs c 0" |
|
296 by (auto dest: succs_iexec1) |
|
297 ultimately |
|
298 have "j0 \<in> exits c" by (simp add: exits_def) |
|
299 with c j0 rest |
|
300 have ?case by fastsimp |
|
301 } |
|
302 ultimately |
|
303 show ?case by cases |
|
304 qed |
|
305 |
|
306 lemma exec_n_drop_right: |
|
307 shows "\<lbrakk> c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s'); j \<notin> {0..<isize c} \<rbrakk> \<Longrightarrow> |
|
308 \<exists>s'' i' k m. |
|
309 (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0 |
|
310 else |
|
311 c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and> |
|
312 i' \<in> exits c) \<and> |
|
313 c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and> |
|
314 n = k + m" |
|
315 by (cases "c = []") |
|
316 (auto dest: exec_n_split [where P="[]", simplified]) |
|
317 |
|
318 |
|
319 text {* |
|
320 Dropping the left context of a potentially incomplete execution of @{term c}. |
|
321 *} |
|
322 |
|
323 lemma exec1_drop_left: |
|
324 assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "isize P1 \<le> i" |
|
325 shows "P2 \<turnstile> (i - isize P1, s, stk) \<rightarrow> (n - isize P1, s', stk')" |
|
326 proof - |
|
327 have "i = isize P1 + (i - isize P1)" by simp |
|
328 then obtain i' where "i = isize P1 + i'" .. |
|
329 moreover |
|
330 have "n = isize P1 + (n - isize P1)" by simp |
|
331 then obtain n' where "n = isize P1 + n'" .. |
|
332 ultimately |
|
333 show ?thesis using assms by clarsimp |
|
334 qed |
|
335 |
|
336 lemma exec_n_drop_left: |
|
337 "\<lbrakk> P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk'); |
|
338 isize P \<le> i; exits P' \<subseteq> {0..} \<rbrakk> \<Longrightarrow> |
|
339 P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')" |
|
340 proof (induct k arbitrary: i s stk) |
|
341 case 0 thus ?case by simp |
|
342 next |
|
343 case (Suc k) |
|
344 from Suc.prems |
|
345 obtain i' s'' stk'' where |
|
346 step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and |
|
347 rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')" |
|
348 by auto |
|
349 from step `isize P \<le> i` |
|
350 have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')" |
|
351 by (rule exec1_drop_left) |
|
352 also |
|
353 then have "i' - isize P \<in> succs P' 0" |
|
354 by (fastsimp dest!: succs_iexec1) |
|
355 with `exits P' \<subseteq> {0..}` |
|
356 have "isize P \<le> i'" by (auto simp: exits_def) |
|
357 from rest this `exits P' \<subseteq> {0..}` |
|
358 have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')" |
|
359 by (rule Suc.hyps) |
|
360 finally |
|
361 show ?case . |
|
362 qed |
|
363 |
|
364 lemmas exec_n_drop_Cons = |
|
365 exec_n_drop_left [where P="[instr]", simplified, standard] |
|
366 |
|
367 definition |
|
368 "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}" |
|
369 |
|
370 lemma ccomp_closed [simp, intro!]: "closed (ccomp c)" |
|
371 using ccomp_exits by (auto simp: closed_def) |
|
372 |
|
373 lemma acomp_closed [simp, intro!]: "closed (acomp c)" |
|
374 by (simp add: closed_def) |
|
375 |
|
376 lemma exec_n_split_full: |
|
377 assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')" |
|
378 assumes P: "isize P \<le> j" |
|
379 assumes closed: "closed P" |
|
380 assumes exits: "exits P' \<subseteq> {0..}" |
|
381 shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'') \<and> |
|
382 P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')" |
|
383 proof (cases "P") |
|
384 case Nil with exec |
|
385 show ?thesis by fastsimp |
|
386 next |
|
387 case Cons |
|
388 hence "0 < isize P" by simp |
|
389 with exec P closed |
|
390 obtain k1 k2 s'' stk'' where |
|
391 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'')" and |
|
392 2: "P @ P' \<turnstile> (isize P,s'',stk'') \<rightarrow>^k2 (j, s', stk')" |
|
393 by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] |
|
394 simp: closed_def) |
|
395 moreover |
|
396 have "j = isize P + (j - isize P)" by simp |
|
397 then obtain j0 where "j = isize P + j0" .. |
|
398 ultimately |
|
399 show ?thesis using exits |
|
400 by (fastsimp dest: exec_n_drop_left) |
|
401 qed |
|
402 |
|
403 |
|
404 subsection {* Correctness theorem *} |
|
405 |
|
406 lemma acomp_neq_Nil [simp]: |
|
407 "acomp a \<noteq> []" |
|
408 by (induct a) auto |
|
409 |
|
410 lemma acomp_exec_n [dest!]: |
|
411 "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow> |
|
412 s' = s \<and> stk' = aval a s#stk" |
|
413 proof (induct a arbitrary: n s' stk stk') |
|
414 case (Plus a1 a2) |
|
415 let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)" |
|
416 from Plus.prems |
|
417 have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" |
|
418 by (simp add: algebra_simps) |
|
419 |
|
420 then obtain n1 s1 stk1 n2 s2 stk2 n3 where |
|
421 "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (isize (acomp a1), s1, stk1)" |
|
422 "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (isize (acomp a2), s2, stk2)" |
|
423 "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')" |
|
424 by (auto dest!: exec_n_split_full) |
|
425 |
|
426 thus ?case by (fastsimp dest: Plus.hyps simp: exec_n_simps) |
|
427 qed (auto simp: exec_n_simps) |
|
428 |
|
429 lemma bcomp_split: |
|
430 shows "\<lbrakk> bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk'); |
|
431 j \<notin> {0..<isize (bcomp b c i)}; 0 \<le> i \<rbrakk> \<Longrightarrow> |
|
432 \<exists>s'' stk'' i' k m. |
|
433 bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and> |
|
434 (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and> |
|
435 bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and> |
|
436 n = k + m" |
|
437 by (cases "bcomp b c i = []") |
|
438 (fastsimp dest!: exec_n_drop_right)+ |
|
439 |
|
440 lemma bcomp_exec_n [dest]: |
|
441 "\<lbrakk> bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk'); |
|
442 isize (bcomp b c j) \<le> i; 0 \<le> j \<rbrakk> \<Longrightarrow> |
|
443 i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and> |
|
444 s' = s \<and> stk' = stk" |
|
445 proof (induct b arbitrary: c j i n s' stk') |
|
446 case B thus ?case |
|
447 by (simp split: split_if_asm add: exec_n_simps) |
|
448 next |
|
449 case (Not b) |
|
450 from Not.prems show ?case |
|
451 by (fastsimp dest!: Not.hyps) |
|
452 next |
|
453 case (And b1 b2) |
|
454 |
|
455 let ?b2 = "bcomp b2 c j" |
|
456 let ?m = "if c then isize ?b2 else isize ?b2 + j" |
|
457 let ?b1 = "bcomp b1 False ?m" |
|
458 |
|
459 have j: "isize (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+ |
|
460 |
|
461 from And.prems |
|
462 obtain s'' stk'' i' k m where |
|
463 b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')" |
|
464 "i' = isize ?b1 \<or> i' = ?m + isize ?b1" and |
|
465 b2: "?b2 \<turnstile> (i' - isize ?b1, s'', stk'') \<rightarrow>^m (i - isize ?b1, s', stk')" |
|
466 by (auto dest!: bcomp_split dest: exec_n_drop_left) |
|
467 from b1 j |
|
468 have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk" |
|
469 by (auto dest!: And.hyps) |
|
470 with b2 j |
|
471 show ?case |
|
472 by (fastsimp dest!: And.hyps simp: exec_n_end split: split_if_asm) |
|
473 next |
|
474 case Less |
|
475 thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) |
|
476 qed |
|
477 |
|
478 lemma ccomp_empty [elim!]: |
|
479 "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s" |
|
480 by (induct c) auto |
|
481 |
|
482 lemma assign [simp]: |
|
483 "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))" |
|
484 by auto |
|
485 |
|
486 lemma ccomp_exec_n: |
|
487 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk') |
|
488 \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk" |
|
489 proof (induct c arbitrary: s t stk stk' n) |
|
490 case SKIP |
|
491 thus ?case by auto |
|
492 next |
|
493 case (Assign x a) |
|
494 thus ?case |
|
495 by simp (fastsimp dest!: exec_n_split_full simp: exec_n_simps) |
|
496 next |
|
497 case (Semi c1 c2) |
|
498 thus ?case by (fastsimp dest!: exec_n_split_full) |
|
499 next |
|
500 case (If b c1 c2) |
|
501 note If.hyps [dest!] |
|
502 |
|
503 let ?if = "IF b THEN c1 ELSE c2" |
|
504 let ?cs = "ccomp ?if" |
|
505 let ?bcomp = "bcomp b False (isize (ccomp c1) + 1)" |
|
506 |
|
507 from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (isize ?cs,t,stk')` |
|
508 obtain i' k m s'' stk'' where |
|
509 cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (isize ?cs,t,stk')" and |
|
510 "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" |
|
511 "i' = isize ?bcomp \<or> i' = isize ?bcomp + isize (ccomp c1) + 1" |
|
512 by (auto dest!: bcomp_split) |
|
513 |
|
514 hence i': |
|
515 "s''=s" "stk'' = stk" |
|
516 "i' = (if bval b s then isize ?bcomp else isize ?bcomp+isize(ccomp c1)+1)" |
|
517 by auto |
|
518 |
|
519 with cs have cs': |
|
520 "ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile> |
|
521 (if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m |
|
522 (1 + isize (ccomp c1) + isize (ccomp c2), t, stk')" |
|
523 by (fastsimp dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps) |
|
524 |
|
525 show ?case |
|
526 proof (cases "bval b s") |
|
527 case True with cs' |
|
528 show ?thesis |
|
529 by simp |
|
530 (fastsimp dest: exec_n_drop_right |
|
531 split: split_if_asm simp: exec_n_simps) |
|
532 next |
|
533 case False with cs' |
|
534 show ?thesis |
|
535 by (auto dest!: exec_n_drop_Cons exec_n_drop_left |
|
536 simp: exits_Cons isuccs_def) |
|
537 qed |
|
538 next |
|
539 case (While b c) |
|
540 |
|
541 from While.prems |
|
542 show ?case |
|
543 proof (induct n arbitrary: s rule: nat_less_induct) |
|
544 case (1 n) |
|
545 |
|
546 { assume "\<not> bval b s" |
|
547 with "1.prems" |
|
548 have ?case |
|
549 by simp |
|
550 (fastsimp dest!: bcomp_exec_n bcomp_split |
|
551 simp: exec_n_simps) |
|
552 } moreover { |
|
553 assume b: "bval b s" |
|
554 let ?c0 = "WHILE b DO c" |
|
555 let ?cs = "ccomp ?c0" |
|
556 let ?bs = "bcomp b False (isize (ccomp c) + 1)" |
|
557 let ?jmp = "[JMPB (isize ?bs + isize (ccomp c) + 1)]" |
|
558 |
|
559 from "1.prems" b |
|
560 obtain k where |
|
561 cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and |
|
562 k: "k \<le> n" |
|
563 by (fastsimp dest!: bcomp_split) |
|
564 |
|
565 have ?case |
|
566 proof cases |
|
567 assume "ccomp c = []" |
|
568 with cs k |
|
569 obtain m where |
|
570 "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')" |
|
571 "m < n" |
|
572 by (auto simp: exec_n_step [where k=k]) |
|
573 with "1.hyps" |
|
574 show ?case by blast |
|
575 next |
|
576 assume "ccomp c \<noteq> []" |
|
577 with cs |
|
578 obtain m m' s'' stk'' where |
|
579 c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (isize (ccomp c), s'', stk'')" and |
|
580 rest: "?cs \<turnstile> (isize ?bs + isize (ccomp c), s'', stk'') \<rightarrow>^m |
|
581 (isize ?cs, t, stk')" and |
|
582 m: "k = m + m'" |
|
583 by (auto dest: exec_n_split [where i=0, simplified]) |
|
584 from c |
|
585 have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk" |
|
586 by (auto dest!: While.hyps) |
|
587 moreover |
|
588 from rest m k stk |
|
589 obtain k' where |
|
590 "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')" |
|
591 "k' < n" |
|
592 by (auto simp: exec_n_step [where k=m]) |
|
593 with "1.hyps" |
|
594 have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast |
|
595 ultimately |
|
596 show ?case using b by blast |
|
597 qed |
|
598 } |
|
599 ultimately show ?case by cases |
|
600 qed |
|
601 qed |
|
602 |
|
603 theorem ccomp_exec: |
|
604 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t" |
|
605 by (auto dest: exec_exec_n ccomp_exec_n) |
|
606 |
|
607 corollary ccomp_sound: |
|
608 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk) \<longleftrightarrow> (c,s) \<Rightarrow> t" |
|
609 by (blast intro!: ccomp_exec ccomp_bigstep) |
|
610 |
|
611 end |