1.1 --- a/src/HOL/IMP/Comp_Rev.thy Sat Feb 23 22:00:12 2013 +0100
1.2 +++ b/src/HOL/IMP/Comp_Rev.thy Sun Feb 24 13:46:14 2013 +1100
1.3 @@ -1,3 +1,5 @@
1.4 +(* Author: Gerwin Klein *)
1.5 +
1.6 theory Comp_Rev
1.7 imports Compiler
1.8 begin
1.9 @@ -14,7 +16,7 @@
1.10 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
1.11 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
1.12
1.13 -text {* The possible successor pc's of an instruction at position @{term n} *}
1.14 +text {* The possible successor PCs of an instruction at position @{term n} *}
1.15 definition
1.16 "isuccs i n \<equiv> case i of
1.17 JMP j \<Rightarrow> {n + 1 + j}
1.18 @@ -22,13 +24,14 @@
1.19 | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
1.20 | _ \<Rightarrow> {n +1}"
1.21
1.22 -text {* The possible successors pc's of an instruction list *}
1.23 +text {* The possible successors PCs of an instruction list *}
1.24 definition
1.25 - "succs P n = {s. \<exists>i. 0 \<le> i \<and> i < isize P \<and> s \<in> isuccs (P!!i) (n+i)}"
1.26 + succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
1.27 + "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}"
1.28
1.29 -text {* Possible exit pc's of a program *}
1.30 +text {* Possible exit PCs of a program *}
1.31 definition
1.32 - "exits P = succs P 0 - {0..< isize P}"
1.33 + "exits P = succs P 0 - {0..< size P}"
1.34
1.35
1.36 subsection {* Basic properties of @{term exec_n} *}
1.37 @@ -69,11 +72,11 @@
1.38 by (cases k) auto
1.39
1.40 lemma exec1_end:
1.41 - "isize P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
1.42 + "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
1.43 by auto
1.44
1.45 lemma exec_n_end:
1.46 - "isize P <= n \<Longrightarrow>
1.47 + "size P <= (n::int) \<Longrightarrow>
1.48 P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
1.49 by (cases k) (auto simp: exec1_end)
1.50
1.51 @@ -98,9 +101,9 @@
1.52 lemma succs_Cons:
1.53 "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
1.54 proof
1.55 - let ?isuccs = "\<lambda>p P n i. 0 \<le> i \<and> i < isize P \<and> p \<in> isuccs (P!!i) (n+i)"
1.56 + let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
1.57 { fix p assume "p \<in> succs (x#xs) n"
1.58 - then obtain i where isuccs: "?isuccs p (x#xs) n i"
1.59 + then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
1.60 unfolding succs_def by auto
1.61 have "p \<in> ?x \<union> ?xs"
1.62 proof cases
1.63 @@ -132,7 +135,7 @@
1.64 qed
1.65
1.66 lemma succs_iexec1:
1.67 - assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < isize P"
1.68 + assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
1.69 shows "fst c' \<in> succs P 0"
1.70 using assms by (auto simp: succs_def isuccs_def split: instr.split)
1.71
1.72 @@ -149,13 +152,13 @@
1.73 by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)
1.74
1.75 lemma succs_append [simp]:
1.76 - "succs (xs @ ys) n = succs xs n \<union> succs ys (n + isize xs)"
1.77 + "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
1.78 by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)
1.79
1.80
1.81 lemma exits_append [simp]:
1.82 - "exits (xs @ ys) = exits xs \<union> (op + (isize xs)) ` exits ys -
1.83 - {0..<isize xs + isize ys}"
1.84 + "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys -
1.85 + {0..<size xs + size ys}"
1.86 by (auto simp: exits_def image_set_diff)
1.87
1.88 lemma exits_single:
1.89 @@ -164,7 +167,7 @@
1.90
1.91 lemma exits_Cons:
1.92 "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs -
1.93 - {0..<1 + isize xs}"
1.94 + {0..<1 + size xs}"
1.95 using exits_append [of "[x]" xs]
1.96 by (simp add: exits_single)
1.97
1.98 @@ -181,21 +184,21 @@
1.99 by (auto simp: exits_def)
1.100
1.101 lemma acomp_succs [simp]:
1.102 - "succs (acomp a) n = {n + 1 .. n + isize (acomp a)}"
1.103 + "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
1.104 by (induct a arbitrary: n) auto
1.105
1.106 lemma acomp_size:
1.107 - "1 \<le> isize (acomp a)"
1.108 + "(1::int) \<le> size (acomp a)"
1.109 by (induct a) auto
1.110
1.111 lemma acomp_exits [simp]:
1.112 - "exits (acomp a) = {isize (acomp a)}"
1.113 + "exits (acomp a) = {size (acomp a)}"
1.114 by (auto simp: exits_def acomp_size)
1.115
1.116 lemma bcomp_succs:
1.117 "0 \<le> i \<Longrightarrow>
1.118 - succs (bcomp b c i) n \<subseteq> {n .. n + isize (bcomp b c i)}
1.119 - \<union> {n + i + isize (bcomp b c i)}"
1.120 + succs (bcomp b c i) n \<subseteq> {n .. n + size (bcomp b c i)}
1.121 + \<union> {n + i + size (bcomp b c i)}"
1.122 proof (induction b arbitrary: c i n)
1.123 case (And b1 b2)
1.124 from And.prems
1.125 @@ -208,17 +211,19 @@
1.126 lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
1.127
1.128 lemma bcomp_exits:
1.129 + fixes i :: int
1.130 + shows
1.131 "0 \<le> i \<Longrightarrow>
1.132 - exits (bcomp b c i) \<subseteq> {isize (bcomp b c i), i + isize (bcomp b c i)}"
1.133 + exits (bcomp b c i) \<subseteq> {size (bcomp b c i), i + size (bcomp b c i)}"
1.134 by (auto simp: exits_def)
1.135
1.136 lemma bcomp_exitsD [dest!]:
1.137 "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow>
1.138 - p = isize (bcomp b c i) \<or> p = i + isize (bcomp b c i)"
1.139 + p = size (bcomp b c i) \<or> p = i + size (bcomp b c i)"
1.140 using bcomp_exits by auto
1.141
1.142 lemma ccomp_succs:
1.143 - "succs (ccomp c) n \<subseteq> {n..n + isize (ccomp c)}"
1.144 + "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}"
1.145 proof (induction c arbitrary: n)
1.146 case SKIP thus ?case by simp
1.147 next
1.148 @@ -240,58 +245,61 @@
1.149 qed
1.150
1.151 lemma ccomp_exits:
1.152 - "exits (ccomp c) \<subseteq> {isize (ccomp c)}"
1.153 + "exits (ccomp c) \<subseteq> {size (ccomp c)}"
1.154 using ccomp_succs [of c 0] by (auto simp: exits_def)
1.155
1.156 lemma ccomp_exitsD [dest!]:
1.157 - "p \<in> exits (ccomp c) \<Longrightarrow> p = isize (ccomp c)"
1.158 + "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)"
1.159 using ccomp_exits by auto
1.160
1.161
1.162 subsection {* Splitting up machine executions *}
1.163
1.164 lemma exec1_split:
1.165 - "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize c \<Longrightarrow>
1.166 - c \<turnstile> (i,s) \<rightarrow> (j - isize P, s')"
1.167 + fixes i j :: int
1.168 + shows
1.169 + "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow>
1.170 + c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
1.171 by (auto split: instr.splits)
1.172
1.173 lemma exec_n_split:
1.174 - assumes "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow>^n (j, s')"
1.175 - "0 \<le> i" "i < isize c"
1.176 - "j \<notin> {isize P ..< isize P + isize c}"
1.177 - shows "\<exists>s'' i' k m.
1.178 + fixes i j :: int
1.179 + assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
1.180 + "0 \<le> i" "i < size c"
1.181 + "j \<notin> {size P ..< size P + size c}"
1.182 + shows "\<exists>s'' (i'::int) k m.
1.183 c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
1.184 i' \<in> exits c \<and>
1.185 - P @ c @ P' \<turnstile> (isize P + i', s'') \<rightarrow>^m (j, s') \<and>
1.186 + P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and>
1.187 n = k + m"
1.188 using assms proof (induction n arbitrary: i j s)
1.189 case 0
1.190 thus ?case by simp
1.191 next
1.192 case (Suc n)
1.193 - have i: "0 \<le> i" "i < isize c" by fact+
1.194 + have i: "0 \<le> i" "i < size c" by fact+
1.195 from Suc.prems
1.196 - have j: "\<not> (isize P \<le> j \<and> j < isize P + isize c)" by simp
1.197 + have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp
1.198 from Suc.prems
1.199 obtain i0 s0 where
1.200 - step: "P @ c @ P' \<turnstile> (isize P + i, s) \<rightarrow> (i0,s0)" and
1.201 + step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and
1.202 rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
1.203 by clarsimp
1.204
1.205 from step i
1.206 - have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - isize P, s0)" by (rule exec1_split)
1.207 + have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split)
1.208
1.209 - have "i0 = isize P + (i0 - isize P) " by simp
1.210 - then obtain j0 where j0: "i0 = isize P + j0" ..
1.211 + have "i0 = size P + (i0 - size P) " by simp
1.212 + then obtain j0::int where j0: "i0 = size P + j0" ..
1.213
1.214 note split_paired_Ex [simp del]
1.215
1.216 - { assume "j0 \<in> {0 ..< isize c}"
1.217 + { assume "j0 \<in> {0 ..< size c}"
1.218 with j0 j rest c
1.219 have ?case
1.220 by (fastforce dest!: Suc.IH intro!: exec_Suc)
1.221 } moreover {
1.222 - assume "j0 \<notin> {0 ..< isize c}"
1.223 + assume "j0 \<notin> {0 ..< size c}"
1.224 moreover
1.225 from c j0 have "j0 \<in> succs c 0"
1.226 by (auto dest: succs_iexec1 simp del: iexec.simps)
1.227 @@ -305,7 +313,8 @@
1.228 qed
1.229
1.230 lemma exec_n_drop_right:
1.231 - assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<isize c}"
1.232 + fixes j :: int
1.233 + assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}"
1.234 shows "\<exists>s'' i' k m.
1.235 (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
1.236 else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
1.237 @@ -322,22 +331,24 @@
1.238 *}
1.239
1.240 lemma exec1_drop_left:
1.241 - assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "isize P1 \<le> i"
1.242 - shows "P2 \<turnstile> (i - isize P1, s, stk) \<rightarrow> (n - isize P1, s', stk')"
1.243 + fixes i n :: int
1.244 + assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i"
1.245 + shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')"
1.246 proof -
1.247 - have "i = isize P1 + (i - isize P1)" by simp
1.248 - then obtain i' where "i = isize P1 + i'" ..
1.249 + have "i = size P1 + (i - size P1)" by simp
1.250 + then obtain i' :: int where "i = size P1 + i'" ..
1.251 moreover
1.252 - have "n = isize P1 + (n - isize P1)" by simp
1.253 - then obtain n' where "n = isize P1 + n'" ..
1.254 + have "n = size P1 + (n - size P1)" by simp
1.255 + then obtain n' :: int where "n = size P1 + n'" ..
1.256 ultimately
1.257 show ?thesis using assms by (clarsimp simp del: iexec.simps)
1.258 qed
1.259
1.260 lemma exec_n_drop_left:
1.261 + fixes i n :: int
1.262 assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
1.263 - "isize P \<le> i" "exits P' \<subseteq> {0..}"
1.264 - shows "P' \<turnstile> (i - isize P, s, stk) \<rightarrow>^k (n - isize P, s', stk')"
1.265 + "size P \<le> i" "exits P' \<subseteq> {0..}"
1.266 + shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')"
1.267 using assms proof (induction k arbitrary: i s stk)
1.268 case 0 thus ?case by simp
1.269 next
1.270 @@ -347,16 +358,16 @@
1.271 step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
1.272 rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
1.273 by (auto simp del: exec1_def)
1.274 - from step `isize P \<le> i`
1.275 - have "P' \<turnstile> (i - isize P, s, stk) \<rightarrow> (i' - isize P, s'', stk'')"
1.276 + from step `size P \<le> i`
1.277 + have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')"
1.278 by (rule exec1_drop_left)
1.279 moreover
1.280 - then have "i' - isize P \<in> succs P' 0"
1.281 + then have "i' - size P \<in> succs P' 0"
1.282 by (fastforce dest!: succs_iexec1 simp del: iexec.simps)
1.283 with `exits P' \<subseteq> {0..}`
1.284 - have "isize P \<le> i'" by (auto simp: exits_def)
1.285 + have "size P \<le> i'" by (auto simp: exits_def)
1.286 from rest this `exits P' \<subseteq> {0..}`
1.287 - have "P' \<turnstile> (i' - isize P, s'', stk'') \<rightarrow>^k (n - isize P, s', stk')"
1.288 + have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
1.289 by (rule Suc.IH)
1.290 ultimately
1.291 show ?case by auto
1.292 @@ -366,7 +377,7 @@
1.293 exec_n_drop_left [where P="[instr]", simplified] for instr
1.294
1.295 definition
1.296 - "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}"
1.297 + "closed P \<longleftrightarrow> exits P \<subseteq> {size P}"
1.298
1.299 lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
1.300 using ccomp_exits by (auto simp: closed_def)
1.301 @@ -375,27 +386,28 @@
1.302 by (simp add: closed_def)
1.303
1.304 lemma exec_n_split_full:
1.305 + fixes j :: int
1.306 assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
1.307 - assumes P: "isize P \<le> j"
1.308 + assumes P: "size P \<le> j"
1.309 assumes closed: "closed P"
1.310 assumes exits: "exits P' \<subseteq> {0..}"
1.311 - shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'') \<and>
1.312 - P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')"
1.313 + shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and>
1.314 + P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')"
1.315 proof (cases "P")
1.316 case Nil with exec
1.317 show ?thesis by fastforce
1.318 next
1.319 case Cons
1.320 - hence "0 < isize P" by simp
1.321 + hence "0 < size P" by simp
1.322 with exec P closed
1.323 obtain k1 k2 s'' stk'' where
1.324 - 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (isize P, s'', stk'')" and
1.325 - 2: "P @ P' \<turnstile> (isize P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
1.326 + 1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and
1.327 + 2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
1.328 by (auto dest!: exec_n_split [where P="[]" and i=0, simplified]
1.329 simp: closed_def)
1.330 moreover
1.331 - have "j = isize P + (j - isize P)" by simp
1.332 - then obtain j0 where "j = isize P + j0" ..
1.333 + have "j = size P + (j - size P)" by simp
1.334 + then obtain j0 :: int where "j = size P + j0" ..
1.335 ultimately
1.336 show ?thesis using exits
1.337 by (fastforce dest: exec_n_drop_left)
1.338 @@ -409,18 +421,18 @@
1.339 by (induct a) auto
1.340
1.341 lemma acomp_exec_n [dest!]:
1.342 - "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (isize (acomp a),s',stk') \<Longrightarrow>
1.343 + "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow>
1.344 s' = s \<and> stk' = aval a s#stk"
1.345 proof (induction a arbitrary: n s' stk stk')
1.346 case (Plus a1 a2)
1.347 - let ?sz = "isize (acomp a1) + (isize (acomp a2) + 1)"
1.348 + let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
1.349 from Plus.prems
1.350 have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')"
1.351 by (simp add: algebra_simps)
1.352
1.353 then obtain n1 s1 stk1 n2 s2 stk2 n3 where
1.354 - "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (isize (acomp a1), s1, stk1)"
1.355 - "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (isize (acomp a2), s2, stk2)"
1.356 + "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
1.357 + "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)"
1.358 "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
1.359 by (auto dest!: exec_n_split_full)
1.360
1.361 @@ -428,19 +440,21 @@
1.362 qed (auto simp: exec_n_simps)
1.363
1.364 lemma bcomp_split:
1.365 + fixes i j :: int
1.366 assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')"
1.367 - "j \<notin> {0..<isize (bcomp b c i)}" "0 \<le> i"
1.368 - shows "\<exists>s'' stk'' i' k m.
1.369 + "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i"
1.370 + shows "\<exists>s'' stk'' (i'::int) k m.
1.371 bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
1.372 - (i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
1.373 + (i' = size (bcomp b c i) \<or> i' = i + size (bcomp b c i)) \<and>
1.374 bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
1.375 n = k + m"
1.376 using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+
1.377
1.378 lemma bcomp_exec_n [dest]:
1.379 + fixes i j :: int
1.380 assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
1.381 - "isize (bcomp b c j) \<le> i" "0 \<le> j"
1.382 - shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
1.383 + "size (bcomp b c j) \<le> i" "0 \<le> j"
1.384 + shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and>
1.385 s' = s \<and> stk' = stk"
1.386 using assms proof (induction b arbitrary: c j i n s' stk')
1.387 case Bc thus ?case
1.388 @@ -453,19 +467,19 @@
1.389 case (And b1 b2)
1.390
1.391 let ?b2 = "bcomp b2 c j"
1.392 - let ?m = "if c then isize ?b2 else isize ?b2 + j"
1.393 + let ?m = "if c then size ?b2 else size ?b2 + j"
1.394 let ?b1 = "bcomp b1 False ?m"
1.395
1.396 - have j: "isize (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+
1.397 + have j: "size (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+
1.398
1.399 from And.prems
1.400 - obtain s'' stk'' i' k m where
1.401 + obtain s'' stk'' and i'::int and k m where
1.402 b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')"
1.403 - "i' = isize ?b1 \<or> i' = ?m + isize ?b1" and
1.404 - b2: "?b2 \<turnstile> (i' - isize ?b1, s'', stk'') \<rightarrow>^m (i - isize ?b1, s', stk')"
1.405 + "i' = size ?b1 \<or> i' = ?m + size ?b1" and
1.406 + b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')"
1.407 by (auto dest!: bcomp_split dest: exec_n_drop_left)
1.408 from b1 j
1.409 - have "i' = isize ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
1.410 + have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
1.411 by (auto dest!: And.IH)
1.412 with b2 j
1.413 show ?case
1.414 @@ -482,7 +496,7 @@
1.415 declare assign_simp [simp]
1.416
1.417 lemma ccomp_exec_n:
1.418 - "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
1.419 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk')
1.420 \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
1.421 proof (induction c arbitrary: s t stk stk' n)
1.422 case SKIP
1.423 @@ -500,24 +514,24 @@
1.424
1.425 let ?if = "IF b THEN c1 ELSE c2"
1.426 let ?cs = "ccomp ?if"
1.427 - let ?bcomp = "bcomp b False (isize (ccomp c1) + 1)"
1.428 + let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"
1.429
1.430 - from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (isize ?cs,t,stk')`
1.431 - obtain i' k m s'' stk'' where
1.432 - cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (isize ?cs,t,stk')" and
1.433 + from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')`
1.434 + obtain i' :: int and k m s'' stk'' where
1.435 + cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and
1.436 "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')"
1.437 - "i' = isize ?bcomp \<or> i' = isize ?bcomp + isize (ccomp c1) + 1"
1.438 + "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1"
1.439 by (auto dest!: bcomp_split)
1.440
1.441 hence i':
1.442 "s''=s" "stk'' = stk"
1.443 - "i' = (if bval b s then isize ?bcomp else isize ?bcomp+isize(ccomp c1)+1)"
1.444 + "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
1.445 by auto
1.446
1.447 with cs have cs':
1.448 - "ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile>
1.449 - (if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m
1.450 - (1 + isize (ccomp c1) + isize (ccomp c2), t, stk')"
1.451 + "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile>
1.452 + (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m
1.453 + (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
1.454 by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
1.455
1.456 show ?case
1.457 @@ -551,12 +565,12 @@
1.458 assume b: "bval b s"
1.459 let ?c0 = "WHILE b DO c"
1.460 let ?cs = "ccomp ?c0"
1.461 - let ?bs = "bcomp b False (isize (ccomp c) + 1)"
1.462 - let ?jmp = "[JMP (-((isize ?bs + isize (ccomp c) + 1)))]"
1.463 + let ?bs = "bcomp b False (size (ccomp c) + 1)"
1.464 + let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"
1.465
1.466 from "1.prems" b
1.467 obtain k where
1.468 - cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and
1.469 + cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and
1.470 k: "k \<le> n"
1.471 by (fastforce dest!: bcomp_split)
1.472
1.473 @@ -565,7 +579,7 @@
1.474 assume "ccomp c = []"
1.475 with cs k
1.476 obtain m where
1.477 - "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (isize (ccomp ?c0), t, stk')"
1.478 + "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
1.479 "m < n"
1.480 by (auto simp: exec_n_step [where k=k])
1.481 with "1.IH"
1.482 @@ -574,9 +588,9 @@
1.483 assume "ccomp c \<noteq> []"
1.484 with cs
1.485 obtain m m' s'' stk'' where
1.486 - c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (isize (ccomp c), s'', stk'')" and
1.487 - rest: "?cs \<turnstile> (isize ?bs + isize (ccomp c), s'', stk'') \<rightarrow>^m
1.488 - (isize ?cs, t, stk')" and
1.489 + c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and
1.490 + rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m
1.491 + (size ?cs, t, stk')" and
1.492 m: "k = m + m'"
1.493 by (auto dest: exec_n_split [where i=0, simplified])
1.494 from c
1.495 @@ -585,7 +599,7 @@
1.496 moreover
1.497 from rest m k stk
1.498 obtain k' where
1.499 - "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (isize ?cs, t, stk')"
1.500 + "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
1.501 "k' < n"
1.502 by (auto simp: exec_n_step [where k=m])
1.503 with "1.IH"
1.504 @@ -599,11 +613,11 @@
1.505 qed
1.506
1.507 theorem ccomp_exec:
1.508 - "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
1.509 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
1.510 by (auto dest: exec_exec_n ccomp_exec_n)
1.511
1.512 corollary ccomp_sound:
1.513 - "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk) \<longleftrightarrow> (c,s) \<Rightarrow> t"
1.514 + "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk) \<longleftrightarrow> (c,s) \<Rightarrow> t"
1.515 by (blast intro!: ccomp_exec ccomp_bigstep)
1.516
1.517 end
2.1 --- a/src/HOL/IMP/Compiler.thy Sat Feb 23 22:00:12 2013 +0100
2.2 +++ b/src/HOL/IMP/Compiler.thy Sun Feb 24 13:46:14 2013 +1100
2.3 @@ -1,4 +1,4 @@
2.4 -(* Author: Tobias Nipkow *)
2.5 +(* Author: Tobias Nipkow and Gerwin Klein *)
2.6
2.7 header "Compiler for IMP"
2.8
2.9 @@ -7,25 +7,29 @@
2.10
2.11 subsection "List setup"
2.12
2.13 -text {*
2.14 - We are going to define a small machine language where programs are
2.15 - lists of instructions. For nicer algebraic properties in our lemmas
2.16 - later, we prefer @{typ int} to @{term nat} as program counter.
2.17 -
2.18 - Therefore, we define notation for size and indexing for lists
2.19 - on @{typ int}:
2.20 +text {*
2.21 + In the following, we use the length of lists as integers
2.22 + instead of natural numbers. Instead of converting @{typ nat}
2.23 + to @{typ int} explicitly, we tell Isabelle to coerce @{typ nat}
2.24 + automatically when necessary.
2.25 *}
2.26 -abbreviation "isize xs == int (length xs)"
2.27 +declare [[coercion_enabled]]
2.28 +declare [[coercion "int :: nat \<Rightarrow> int"]]
2.29
2.30 +text {*
2.31 + Similarly, we will want to access the ith element of a list,
2.32 + where @{term i} is an @{typ int}.
2.33 +*}
2.34 fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
2.35 "(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
2.36
2.37 text {*
2.38 - The only additional lemma we need is indexing over append:
2.39 + The only additional lemma we need about this function
2.40 + is indexing over append:
2.41 *}
2.42 lemma inth_append [simp]:
2.43 "0 \<le> n \<Longrightarrow>
2.44 - (xs @ ys) !! n = (if n < isize xs then xs !! n else ys !! (n - isize xs))"
2.45 + (xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))"
2.46 by (induction xs arbitrary: n) (auto simp: algebra_simps)
2.47
2.48 subsection "Instructions and Stack Machine"
2.49 @@ -60,12 +64,12 @@
2.50 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)
2.51 where
2.52 "P \<turnstile> c \<rightarrow> c' =
2.53 - (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < isize P)"
2.54 + (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
2.55
2.56 declare exec1_def [simp]
2.57
2.58 lemma exec1I [intro, code_pred_intro]:
2.59 - "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < isize P
2.60 + "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
2.61 \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
2.62 by simp
2.63
2.64 @@ -107,14 +111,18 @@
2.65 by (induction rule: exec.induct) (fastforce intro: exec1_appendR)+
2.66
2.67 lemma exec1_appendL:
2.68 + fixes i i' :: int
2.69 + shows
2.70 "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
2.71 - P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow> (isize(P')+i',s',stk')"
2.72 -by (auto split: instr.split)
2.73 + P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
2.74 + by (auto split: instr.split)
2.75
2.76 lemma exec_appendL:
2.77 + fixes i i' :: int
2.78 + shows
2.79 "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
2.80 - P' @ P \<turnstile> (isize(P')+i,s,stk) \<rightarrow>* (isize(P')+i',s',stk')"
2.81 -by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
2.82 + P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
2.83 + by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
2.84
2.85 text{* Now we specialise the above lemmas to enable automatic proofs of
2.86 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
2.87 @@ -130,19 +138,23 @@
2.88 by (drule exec_appendL[where P'="[instr]"]) simp
2.89
2.90 lemma exec_appendL_if[intro]:
2.91 - "isize P' <= i
2.92 - \<Longrightarrow> P \<turnstile> (i - isize P',s,stk) \<rightarrow>* (i',s',stk')
2.93 - \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (isize P' + i',s',stk')"
2.94 + fixes i i' :: int
2.95 + shows
2.96 + "size P' <= i
2.97 + \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
2.98 + \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
2.99 by (drule exec_appendL[where P'=P']) simp
2.100
2.101 text{* Split the execution of a compound program up into the excution of its
2.102 parts: *}
2.103
2.104 lemma exec_append_trans[intro]:
2.105 + fixes i' i'' j'' :: int
2.106 + shows
2.107 "P \<turnstile> (0,s,stk) \<rightarrow>* (i',s',stk') \<Longrightarrow>
2.108 - isize P \<le> i' \<Longrightarrow>
2.109 - P' \<turnstile> (i' - isize P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
2.110 - j'' = isize P + i''
2.111 + size P \<le> i' \<Longrightarrow>
2.112 + P' \<turnstile> (i' - size P,s',stk') \<rightarrow>* (i'',s'',stk'') \<Longrightarrow>
2.113 + j'' = size P + i''
2.114 \<Longrightarrow>
2.115 P @ P' \<turnstile> (0,s,stk) \<rightarrow>* (j'',s'',stk'')"
2.116 by(metis exec_trans[OF exec_appendR exec_appendL_if])
2.117 @@ -159,7 +171,7 @@
2.118 "acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"
2.119
2.120 lemma acomp_correct[intro]:
2.121 - "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
2.122 + "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
2.123 by (induction a arbitrary: stk) fastforce+
2.124
2.125 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
2.126 @@ -167,7 +179,7 @@
2.127 "bcomp (Not b) c n = bcomp b (\<not>c) n" |
2.128 "bcomp (And b1 b2) c n =
2.129 (let cb2 = bcomp b2 c n;
2.130 - m = (if c then isize cb2 else isize cb2+n);
2.131 + m = (if c then size cb2 else (size cb2::int)+n);
2.132 cb1 = bcomp b1 False m
2.133 in cb1 @ cb2)" |
2.134 "bcomp (Less a1 a2) c n =
2.135 @@ -178,15 +190,17 @@
2.136 False 3"
2.137
2.138 lemma bcomp_correct[intro]:
2.139 + fixes n :: int
2.140 + shows
2.141 "0 \<le> n \<Longrightarrow>
2.142 bcomp b c n \<turnstile>
2.143 - (0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
2.144 + (0,s,stk) \<rightarrow>* (size(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
2.145 proof(induction b arbitrary: c n)
2.146 case Not
2.147 from Not(1)[where c="~c"] Not(2) show ?case by fastforce
2.148 next
2.149 case (And b1 b2)
2.150 - from And(1)[of "if c then isize(bcomp b2 c n) else isize(bcomp b2 c n) + n"
2.151 + from And(1)[of "if c then size(bcomp b2 c n) else size(bcomp b2 c n) + n"
2.152 "False"]
2.153 And(2)[of n "c"] And(3)
2.154 show ?case by fastforce
2.155 @@ -197,11 +211,11 @@
2.156 "ccomp (x ::= a) = acomp a @ [STORE x]" |
2.157 "ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
2.158 "ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
2.159 - (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (isize cc\<^isub>1 + 1)
2.160 - in cb @ cc\<^isub>1 @ JMP (isize cc\<^isub>2) # cc\<^isub>2)" |
2.161 + (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
2.162 + in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" |
2.163 "ccomp (WHILE b DO c) =
2.164 - (let cc = ccomp c; cb = bcomp b False (isize cc + 1)
2.165 - in cb @ cc @ [JMP (-(isize cb + isize cc + 1))])"
2.166 + (let cc = ccomp c; cb = bcomp b False (size cc + 1)
2.167 + in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
2.168
2.169
2.170 value "ccomp
2.171 @@ -214,34 +228,34 @@
2.172 subsection "Preservation of semantics"
2.173
2.174 lemma ccomp_bigstep:
2.175 - "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
2.176 + "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)"
2.177 proof(induction arbitrary: stk rule: big_step_induct)
2.178 case (Assign x a s)
2.179 show ?case by (fastforce simp:fun_upd_def cong: if_cong)
2.180 next
2.181 case (Seq c1 s1 s2 c2 s3)
2.182 let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
2.183 - have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
2.184 + have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cc1,s2,stk)"
2.185 using Seq.IH(1) by fastforce
2.186 moreover
2.187 - have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
2.188 + have "?cc1 @ ?cc2 \<turnstile> (size ?cc1,s2,stk) \<rightarrow>* (size(?cc1 @ ?cc2),s3,stk)"
2.189 using Seq.IH(2) by fastforce
2.190 ultimately show ?case by simp (blast intro: exec_trans)
2.191 next
2.192 case (WhileTrue b s1 c s2 s3)
2.193 let ?cc = "ccomp c"
2.194 - let ?cb = "bcomp b False (isize ?cc + 1)"
2.195 + let ?cb = "bcomp b False (size ?cc + 1)"
2.196 let ?cw = "ccomp(WHILE b DO c)"
2.197 - have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb,s1,stk)"
2.198 + have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)"
2.199 using `bval b s1` by fastforce
2.200 moreover
2.201 - have "?cw \<turnstile> (isize ?cb,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
2.202 + have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)"
2.203 using WhileTrue.IH(1) by fastforce
2.204 moreover
2.205 - have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
2.206 + have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
2.207 by fastforce
2.208 moreover
2.209 - have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
2.210 + have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
2.211 ultimately show ?case by(blast intro: exec_trans)
2.212 qed fastforce+
2.213