1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/Comp_Rev.thy Fri Jun 17 20:38:43 2011 +0200
1.3 @@ -0,0 +1,611 @@
1.4 +theory Comp_Rev
1.5 +imports Compiler
1.6 +begin
1.7 +
1.8 +section {* Compiler Correctness, 2nd direction *}
1.9 +
1.10 +subsection {* Definitions *}
1.11 +
1.12 +text {* Execution in @{term n} steps for simpler induction *}
1.13 +primrec
1.14 + exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool"
1.15 + ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55)
1.16 +where
1.17 + "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
1.18 + "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
1.19 +
1.20 +text {* The possible successor pc's of an instruction at position @{term n} *}
1.21 +definition
1.22 + "isuccs i n \<equiv> case i of
1.23 + JMP j \<Rightarrow> {n + 1 + j}
1.24 + | JMPFLESS j \<Rightarrow> {n + 1 + j, n + 1}
1.25 + | JMPFGE j \<Rightarrow> {n + 1 + j, n + 1}
1.26 + | _ \<Rightarrow> {n +1}"
1.27 +
1.28 +(* FIXME: _Collect? *)
1.29 +text {* The possible successors pc's of an instruction list *}
1.30 +definition
1.31 + "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}"
1.32 +
1.33 +text {* Possible exit pc's of a program *}
1.34 +definition
1.35 + "exits P = succs P 0 - {0..< isize P}"
1.36 +
1.37 +
1.38 +subsection {* Basic properties of @{term exec_n} *}
1.39 +
1.40 +lemma exec_n_exec:
1.41 + "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
1.42 + by (induct n arbitrary: c) (auto intro: exec.step)
1.43 +
1.44 +lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
1.45 +
1.46 +lemma exec_Suc [trans]:
1.47 + "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''"
1.48 + by (fastsimp simp del: split_paired_Ex)
1.49 +
1.50 +lemma exec_exec_n:
1.51 + "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
1.52 + by (induct rule: exec.induct) (auto intro: exec_Suc)
1.53 +
1.54 +lemma exec_eq_exec_n:
1.55 + "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
1.56 + by (blast intro: exec_exec_n exec_n_exec)
1.57 +
1.58 +lemma exec_n_Nil [simp]:
1.59 + "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
1.60 + by (induct k) auto
1.61 +
1.62 +lemma exec1_exec_n [elim,intro!]:
1.63 + "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
1.64 + by (cases c') simp
1.65 +
1.66 +
1.67 +subsection {* Concrete symbolic execution steps *}
1.68 +
1.69 +lemma exec_n_step:
1.70 + "n \<noteq> n' \<Longrightarrow>
1.71 + P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') =
1.72 + (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
1.73 + by (cases k) auto
1.74 +
1.75 +lemma exec1_end:
1.76 + "isize P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
1.77 + by auto
1.78 +
1.79 +lemma exec_n_end:
1.80 + "isize P <= n \<Longrightarrow>
1.81 + P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
1.82 + by (cases k) (auto simp: exec1_end)
1.83 +
1.84 +lemmas exec_n_simps = exec_n_step exec_n_end
1.85 +
1.86 +
1.87 +subsection {* Basic properties of @{term succs} *}
1.88 +
1.89 +lemma succs_simps [simp]:
1.90 + "succs [ADD] n = {n + 1}"
1.91 + "succs [LOADI v] n = {n + 1}"
1.92 + "succs [LOAD x] n = {n + 1}"
1.93 + "succs [STORE x] n = {n + 1}"
1.94 + "succs [JMP i] n = {n + 1 + i}"
1.95 + "succs [JMPFGE i] n = {n + 1 + i, n + 1}"
1.96 + "succs [JMPFLESS i] n = {n + 1 + i, n + 1}"
1.97 + by (auto simp: succs_def isuccs_def)
1.98 +
1.99 +lemma succs_empty [iff]: "succs [] n = {}"
1.100 + by (simp add: succs_def)
1.101 +
1.102 +lemma succs_Cons:
1.103 + "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
1.104 +proof
1.105 + let ?isuccs = "\<lambda>p P n i. 0 \<le> i \<and> i < isize P \<and> p \<in> isuccs (P!!i) (n+i)"
1.106 + { fix p assume "p \<in> succs (x#xs) n"
1.107 + then obtain i where isuccs: "?isuccs p (x#xs) n i"
1.108 + unfolding succs_def by auto
1.109 + have "p \<in> ?x \<union> ?xs"
1.110 + proof cases
1.111 + assume "i = 0" with isuccs show ?thesis by simp
1.112 + next
1.113 + assume "i \<noteq> 0"
1.114 + with isuccs
1.115 + have "?isuccs p xs (1+n) (i - 1)" by auto
1.116 + hence "p \<in> ?xs" unfolding succs_def by blast
1.117 + thus ?thesis ..
1.118 + qed
1.119 + }
1.120 + thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
1.121 +
1.122 + { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
1.123 + hence "p \<in> succs (x#xs) n"
1.124 + proof
1.125 + assume "p \<in> ?x" thus ?thesis by (fastsimp simp: succs_def)
1.126 + next
1.127 + assume "p \<in> ?xs"
1.128 + then obtain i where "?isuccs p xs (1+n) i"
1.129 + unfolding succs_def by auto
1.130 + hence "?isuccs p (x#xs) n (1+i)"
1.131 + by (simp add: algebra_simps)
1.132 + thus ?thesis unfolding succs_def by blast
1.133 + qed
1.134 + }
1.135 + thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
1.136 +qed
1.137 +
1.138 +lemma succs_iexec1:
1.139 + "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> fst c' \<in> succs P 0"
1.140 + by (auto elim!: iexec1.cases simp: succs_def isuccs_def)
1.141 +
1.142 +lemma succs_shift:
1.143 + "(p - n \<in> succs P 0) = (p \<in> succs P n)"
1.144 + by (fastsimp simp: succs_def isuccs_def split: instr.split)
1.145 +
1.146 +lemma inj_op_plus [simp]:
1.147 + "inj (op + (i::int))"
1.148 + by (metis add_minus_cancel inj_on_inverseI)
1.149 +
1.150 +lemma succs_set_shift [simp]:
1.151 + "op + i ` succs xs 0 = succs xs i"
1.152 + by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)
1.153 +
1.154 +lemma succs_append [simp]:
1.155 + "succs (xs @ ys) n = succs xs n \<union> succs ys (n + isize xs)"
1.156 + by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)
1.157 +
1.158 +
1.159 +lemma exits_append [simp]:
1.160 + "exits (xs @ ys) = exits xs \<union> (op + (isize xs)) ` exits ys -
1.161 + {0..<isize xs + isize ys}"
1.162 + by (auto simp: exits_def image_set_diff)
1.163 +
1.164 +lemma exits_single:
1.165 + "exits [x] = isuccs x 0 - {0}"
1.166 + by (auto simp: exits_def succs_def)
1.167 +
1.168 +lemma exits_Cons:
1.169 + "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs -
1.170 + {0..<1 + isize xs}"
1.171 + using exits_append [of "[x]" xs]
1.172 + by (simp add: exits_single)
1.173 +
1.174 +lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)
1.175 +
1.176 +lemma exits_simps [simp]:
1.177 + "exits [ADD] = {1}"
1.178 + "exits [LOADI v] = {1}"
1.179 + "exits [LOAD x] = {1}"
1.180 + "exits [STORE x] = {1}"
1.181 + "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
1.182 + "i \<noteq> -1 \<Longrightarrow> exits [JMPFGE i] = {1 + i, 1}"
1.183 + "i \<noteq> -1 \<Longrightarrow> exits [JMPFLESS i] = {1 + i, 1}"
1.184 + by (auto simp: exits_def)
1.185 +
1.186 +lemma acomp_succs [simp]:
1.187 + "succs (acomp a) n = {n + 1 .. n + isize (acomp a)}"
1.188 + by (induct a arbitrary: n) auto
1.189 +
1.190 +lemma acomp_size:
1.191 + "1 \<le> isize (acomp a)"
1.192 + by (induct a) auto
1.193 +
1.194 +lemma exits_acomp [simp]:
1.195 + "exits (acomp a) = {isize (acomp a)}"
1.196 + by (auto simp: exits_def acomp_size)
1.197 +
1.198 +lemma bcomp_succs:
1.199 + "0 \<le> i \<Longrightarrow>
1.200 + succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
1.201 + \<union> {n + i + isize (bcomp b c i)}"
1.202 +proof (induct b arbitrary: c i n)
1.203 + case (And b1 b2)
1.204 + from And.prems
1.205 + show ?case
1.206 + by (cases c)
1.207 + (auto dest: And.hyps(1) [THEN subsetD, rotated]
1.208 + And.hyps(2) [THEN subsetD, rotated])
1.209 +qed auto
1.210 +
1.211 +lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
1.212 +
1.213 +lemma bcomp_exits:
1.214 + "0 \<le> i \<Longrightarrow>
1.215 + exits (bcomp b c i) \<subseteq> {isize (bcomp b c i), i + isize (bcomp b c i)}"
1.216 + by (auto simp: exits_def)
1.217 +
1.218 +lemma bcomp_exitsD [dest!]:
1.219 + "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow>
1.220 + p = isize (bcomp b c i) \<or> p = i + isize (bcomp b c i)"
1.221 + using bcomp_exits by auto
1.222 +
1.223 +lemma ccomp_succs:
1.224 + "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
1.225 +proof (induct c arbitrary: n)
1.226 + case SKIP thus ?case by simp
1.227 +next
1.228 + case Assign thus ?case by simp
1.229 +next
1.230 + case (Semi c1 c2)
1.231 + from Semi.prems
1.232 + show ?case
1.233 + by (fastsimp dest: Semi.hyps [THEN subsetD])
1.234 +next
1.235 + case (If b c1 c2)
1.236 + from If.prems
1.237 + show ?case
1.238 + by (auto dest!: If.hyps [THEN subsetD] simp: isuccs_def succs_Cons)
1.239 +next
1.240 + case (While b c)
1.241 + from While.prems
1.242 + show ?case by (auto dest!: While.hyps [THEN subsetD])
1.243 +qed
1.244 +
1.245 +lemma ccomp_exits:
1.246 + "exits (ccomp c) \<subseteq> {isize (ccomp c)}"
1.247 + using ccomp_succs [of c 0] by (auto simp: exits_def)
1.248 +
1.249 +lemma ccomp_exitsD [dest!]:
1.250 + "p \<in> exits (ccomp c) \<Longrightarrow> p = isize (ccomp c)"
1.251 + using ccomp_exits by auto
1.252 +
1.253 +
1.254 +subsection {* Splitting up machine executions *}
1.255 +
1.256 +lemma exec1_split:
1.257 + "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize c \<Longrightarrow>
1.258 + c \<turnstile> (i,s) \<rightarrow> (j - isize P, s')"
1.259 + by (auto elim!: iexec1.cases)
1.260 +
1.261 +lemma exec_n_split:
1.262 + shows "\<lbrakk> P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s');
1.263 + 0 \<le> i; i < isize c; j \<notin> {isize P ..< isize P + isize c} \<rbrakk> \<Longrightarrow>
1.264 + \<exists>s'' i' k m.
1.265 + c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
1.266 + i' \<in> exits c \<and>
1.267 + P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
1.268 + n = k + m"
1.269 +proof (induct n arbitrary: i j s)
1.270 + case 0
1.271 + thus ?case by simp
1.272 +next
1.273 + case (Suc n)
1.274 + have i: "0 \<le> i" "i < isize c" by fact+
1.275 + from Suc.prems
1.276 + have j: "\<not> (isize P \<le> j \<and> j < isize P + isize c)" by simp
1.277 + from Suc.prems
1.278 + obtain i0 s0 where
1.279 + step: "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (i0,s0)" and
1.280 + rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
1.281 + by clarsimp
1.282 +
1.283 + from step i
1.284 + have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - isize P, s0)" by (rule exec1_split)
1.285 +
1.286 + have "i0 = isize P + (i0 - isize P) " by simp
1.287 + then obtain j0 where j0: "i0 = isize P + j0" ..
1.288 +
1.289 + note split_paired_Ex [simp del]
1.290 +
1.291 + { assume "j0 \<in> {0 ..< isize c}"
1.292 + with j0 j rest c
1.293 + have ?case
1.294 + by (fastsimp dest!: Suc.hyps intro!: exec_Suc)
1.295 + } moreover {
1.296 + assume "j0 \<notin> {0 ..< isize c}"
1.297 + moreover
1.298 + from c j0 have "j0 \<in> succs c 0"
1.299 + by (auto dest: succs_iexec1)
1.300 + ultimately
1.301 + have "j0 \<in> exits c" by (simp add: exits_def)
1.302 + with c j0 rest
1.303 + have ?case by fastsimp
1.304 + }
1.305 + ultimately
1.306 + show ?case by cases
1.307 +qed
1.308 +
1.309 +lemma exec_n_drop_right:
1.310 + shows "\<lbrakk> c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s'); j \<notin> {0..<isize c} \<rbrakk> \<Longrightarrow>
1.311 + \<exists>s'' i' k m.
1.312 + (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
1.313 + else
1.314 + c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
1.315 + i' \<in> exits c) \<and>
1.316 + c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
1.317 + n = k + m"
1.318 + by (cases "c = []")
1.319 + (auto dest: exec_n_split [where P="[]", simplified])
1.320 +
1.321 +
1.322 +text {*
1.323 + Dropping the left context of a potentially incomplete execution of @{term c}.
1.324 +*}
1.325 +
1.326 +lemma exec1_drop_left:
1.327 + assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "isize P1 \<le> i"
1.328 + shows "P2 \<turnstile> (i - isize P1, s, stk) \<rightarrow> (n - isize P1, s', stk')"
1.329 +proof -
1.330 + have "i = isize P1 + (i - isize P1)" by simp
1.331 + then obtain i' where "i = isize P1 + i'" ..
1.332 + moreover
1.333 + have "n = isize P1 + (n - isize P1)" by simp
1.334 + then obtain n' where "n = isize P1 + n'" ..
1.335 + ultimately
1.336 + show ?thesis using assms by clarsimp
1.337 +qed
1.338 +
1.339 +lemma exec_n_drop_left:
1.340 + "\<lbrakk> P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk');
1.341 + isize P \<le> i; exits P' \<subseteq> {0..} \<rbrakk> \<Longrightarrow>
1.342 + P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
1.343 +proof (induct k arbitrary: i s stk)
1.344 + case 0 thus ?case by simp
1.345 +next
1.346 + case (Suc k)
1.347 + from Suc.prems
1.348 + obtain i' s'' stk'' where
1.349 + step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
1.350 + rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
1.351 + by auto
1.352 + from step `isize P \<le> i`
1.353 + have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')"
1.354 + by (rule exec1_drop_left)
1.355 + also
1.356 + then have "i' - isize P \<in> succs P' 0"
1.357 + by (fastsimp dest!: succs_iexec1)
1.358 + with `exits P' \<subseteq> {0..}`
1.359 + have "isize P \<le> i'" by (auto simp: exits_def)
1.360 + from rest this `exits P' \<subseteq> {0..}`
1.361 + have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
1.362 + by (rule Suc.hyps)
1.363 + finally
1.364 + show ?case .
1.365 +qed
1.366 +
1.367 +lemmas exec_n_drop_Cons =
1.368 + exec_n_drop_left [where P="[instr]", simplified, standard]
1.369 +
1.370 +definition
1.371 + "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}"
1.372 +
1.373 +lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
1.374 + using ccomp_exits by (auto simp: closed_def)
1.375 +
1.376 +lemma acomp_closed [simp, intro!]: "closed (acomp c)"
1.377 + by (simp add: closed_def)
1.378 +
1.379 +lemma exec_n_split_full:
1.380 + assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
1.381 + assumes P: "isize P \<le> j"
1.382 + assumes closed: "closed P"
1.383 + assumes exits: "exits P' \<subseteq> {0..}"
1.384 + shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'') \<and>
1.385 + P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')"
1.386 +proof (cases "P")
1.387 + case Nil with exec
1.388 + show ?thesis by fastsimp
1.389 +next
1.390 + case Cons
1.391 + hence "0 < isize P" by simp
1.392 + with exec P closed
1.393 + obtain k1 k2 s'' stk'' where
1.394 + 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'')" and
1.395 + 2: "P @ P' \<turnstile> (isize P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
1.396 + by (auto dest!: exec_n_split [where P="[]" and i=0, simplified]
1.397 + simp: closed_def)
1.398 + moreover
1.399 + have "j = isize P + (j - isize P)" by simp
1.400 + then obtain j0 where "j = isize P + j0" ..
1.401 + ultimately
1.402 + show ?thesis using exits
1.403 + by (fastsimp dest: exec_n_drop_left)
1.404 +qed
1.405 +
1.406 +
1.407 +subsection {* Correctness theorem *}
1.408 +
1.409 +lemma acomp_neq_Nil [simp]:
1.410 + "acomp a \<noteq> []"
1.411 + by (induct a) auto
1.412 +
1.413 +lemma acomp_exec_n [dest!]:
1.414 + "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow>
1.415 + s' = s \<and> stk' = aval a s#stk"
1.416 +proof (induct a arbitrary: n s' stk stk')
1.417 + case (Plus a1 a2)
1.418 + let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
1.419 + from Plus.prems
1.420 + have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')"
1.421 + by (simp add: algebra_simps)
1.422 +
1.423 + then obtain n1 s1 stk1 n2 s2 stk2 n3 where
1.424 + "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (isize (acomp a1), s1, stk1)"
1.425 + "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (isize (acomp a2), s2, stk2)"
1.426 + "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
1.427 + by (auto dest!: exec_n_split_full)
1.428 +
1.429 + thus ?case by (fastsimp dest: Plus.hyps simp: exec_n_simps)
1.430 +qed (auto simp: exec_n_simps)
1.431 +
1.432 +lemma bcomp_split:
1.433 + shows "\<lbrakk> bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk');
1.434 + j \<notin> {0..<isize (bcomp b c i)}; 0 \<le> i \<rbrakk> \<Longrightarrow>
1.435 + \<exists>s'' stk'' i' k m.
1.436 + bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
1.437 + (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
1.438 + bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
1.439 + n = k + m"
1.440 + by (cases "bcomp b c i = []")
1.441 + (fastsimp dest!: exec_n_drop_right)+
1.442 +
1.443 +lemma bcomp_exec_n [dest]:
1.444 + "\<lbrakk> bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk');
1.445 + isize (bcomp b c j) \<le> i; 0 \<le> j \<rbrakk> \<Longrightarrow>
1.446 + i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
1.447 + s' = s \<and> stk' = stk"
1.448 +proof (induct b arbitrary: c j i n s' stk')
1.449 + case B thus ?case
1.450 + by (simp split: split_if_asm add: exec_n_simps)
1.451 +next
1.452 + case (Not b)
1.453 + from Not.prems show ?case
1.454 + by (fastsimp dest!: Not.hyps)
1.455 +next
1.456 + case (And b1 b2)
1.457 +
1.458 + let ?b2 = "bcomp b2 c j"
1.459 + let ?m = "if c then isize ?b2 else isize ?b2 + j"
1.460 + let ?b1 = "bcomp b1 False ?m"
1.461 +
1.462 + have j: "isize (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+
1.463 +
1.464 + from And.prems
1.465 + obtain s'' stk'' i' k m where
1.466 + b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')"
1.467 + "i' = isize ?b1 \<or> i' = ?m + isize ?b1" and
1.468 + b2: "?b2 \<turnstile> (i' - isize ?b1, s'', stk'') \<rightarrow>^m (i - isize ?b1, s', stk')"
1.469 + by (auto dest!: bcomp_split dest: exec_n_drop_left)
1.470 + from b1 j
1.471 + have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
1.472 + by (auto dest!: And.hyps)
1.473 + with b2 j
1.474 + show ?case
1.475 + by (fastsimp dest!: And.hyps simp: exec_n_end split: split_if_asm)
1.476 +next
1.477 + case Less
1.478 + thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *)
1.479 +qed
1.480 +
1.481 +lemma ccomp_empty [elim!]:
1.482 + "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
1.483 + by (induct c) auto
1.484 +
1.485 +lemma assign [simp]:
1.486 + "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
1.487 + by auto
1.488 +
1.489 +lemma ccomp_exec_n:
1.490 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
1.491 + \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
1.492 +proof (induct c arbitrary: s t stk stk' n)
1.493 + case SKIP
1.494 + thus ?case by auto
1.495 +next
1.496 + case (Assign x a)
1.497 + thus ?case
1.498 + by simp (fastsimp dest!: exec_n_split_full simp: exec_n_simps)
1.499 +next
1.500 + case (Semi c1 c2)
1.501 + thus ?case by (fastsimp dest!: exec_n_split_full)
1.502 +next
1.503 + case (If b c1 c2)
1.504 + note If.hyps [dest!]
1.505 +
1.506 + let ?if = "IF b THEN c1 ELSE c2"
1.507 + let ?cs = "ccomp ?if"
1.508 + let ?bcomp = "bcomp b False (isize (ccomp c1) + 1)"
1.509 +
1.510 + from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (isize ?cs,t,stk')`
1.511 + obtain i' k m s'' stk'' where
1.512 + cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (isize ?cs,t,stk')" and
1.513 + "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')"
1.514 + "i' = isize ?bcomp \<or> i' = isize ?bcomp + isize (ccomp c1) + 1"
1.515 + by (auto dest!: bcomp_split)
1.516 +
1.517 + hence i':
1.518 + "s''=s" "stk'' = stk"
1.519 + "i' = (if bval b s then isize ?bcomp else isize ?bcomp+isize(ccomp c1)+1)"
1.520 + by auto
1.521 +
1.522 + with cs have cs':
1.523 + "ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile>
1.524 + (if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m
1.525 + (1 + isize (ccomp c1) + isize (ccomp c2), t, stk')"
1.526 + by (fastsimp dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
1.527 +
1.528 + show ?case
1.529 + proof (cases "bval b s")
1.530 + case True with cs'
1.531 + show ?thesis
1.532 + by simp
1.533 + (fastsimp dest: exec_n_drop_right
1.534 + split: split_if_asm simp: exec_n_simps)
1.535 + next
1.536 + case False with cs'
1.537 + show ?thesis
1.538 + by (auto dest!: exec_n_drop_Cons exec_n_drop_left
1.539 + simp: exits_Cons isuccs_def)
1.540 + qed
1.541 +next
1.542 + case (While b c)
1.543 +
1.544 + from While.prems
1.545 + show ?case
1.546 + proof (induct n arbitrary: s rule: nat_less_induct)
1.547 + case (1 n)
1.548 +
1.549 + { assume "\<not> bval b s"
1.550 + with "1.prems"
1.551 + have ?case
1.552 + by simp
1.553 + (fastsimp dest!: bcomp_exec_n bcomp_split
1.554 + simp: exec_n_simps)
1.555 + } moreover {
1.556 + assume b: "bval b s"
1.557 + let ?c0 = "WHILE b DO c"
1.558 + let ?cs = "ccomp ?c0"
1.559 + let ?bs = "bcomp b False (isize (ccomp c) + 1)"
1.560 + let ?jmp = "[JMPB (isize ?bs + isize (ccomp c) + 1)]"
1.561 +
1.562 + from "1.prems" b
1.563 + obtain k where
1.564 + cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and
1.565 + k: "k \<le> n"
1.566 + by (fastsimp dest!: bcomp_split)
1.567 +
1.568 + have ?case
1.569 + proof cases
1.570 + assume "ccomp c = []"
1.571 + with cs k
1.572 + obtain m where
1.573 + "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
1.574 + "m < n"
1.575 + by (auto simp: exec_n_step [where k=k])
1.576 + with "1.hyps"
1.577 + show ?case by blast
1.578 + next
1.579 + assume "ccomp c \<noteq> []"
1.580 + with cs
1.581 + obtain m m' s'' stk'' where
1.582 + c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (isize (ccomp c), s'', stk'')" and
1.583 + rest: "?cs \<turnstile> (isize ?bs + isize (ccomp c), s'', stk'') \<rightarrow>^m
1.584 + (isize ?cs, t, stk')" and
1.585 + m: "k = m + m'"
1.586 + by (auto dest: exec_n_split [where i=0, simplified])
1.587 + from c
1.588 + have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
1.589 + by (auto dest!: While.hyps)
1.590 + moreover
1.591 + from rest m k stk
1.592 + obtain k' where
1.593 + "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
1.594 + "k' < n"
1.595 + by (auto simp: exec_n_step [where k=m])
1.596 + with "1.hyps"
1.597 + have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
1.598 + ultimately
1.599 + show ?case using b by blast
1.600 + qed
1.601 + }
1.602 + ultimately show ?case by cases
1.603 + qed
1.604 +qed
1.605 +
1.606 +theorem ccomp_exec:
1.607 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
1.608 + by (auto dest: exec_exec_n ccomp_exec_n)
1.609 +
1.610 +corollary ccomp_sound:
1.611 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk) \<longleftrightarrow> (c,s) \<Rightarrow> t"
1.612 + by (blast intro!: ccomp_exec ccomp_bigstep)
1.613 +
1.614 +end