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