tuned theory name
authornipkow
Thu Jun 20 17:26:16 2013 +0200 (2013-06-20)
changeset 52400ded7b9c60dc2
parent 52399 7a7d05e2e5c0
child 52401 56e83c57f953
tuned theory name
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMP/Compiler2.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/IMP/Comp_Rev.thy	Thu Jun 20 10:15:34 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,625 +0,0 @@
     1.4 -(* Author: Gerwin Klein *)
     1.5 -
     1.6 -theory Comp_Rev
     1.7 -imports Compiler
     1.8 -begin
     1.9 -
    1.10 -section {* Compiler Correctness, Reverse Direction *}
    1.11 -
    1.12 -subsection {* Definitions *}
    1.13 -
    1.14 -text {* Execution in @{term n} steps for simpler induction *}
    1.15 -primrec 
    1.16 -  exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
    1.17 -  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
    1.18 -where 
    1.19 -  "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
    1.20 -  "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
    1.21 -
    1.22 -text {* The possible successor PCs of an instruction at position @{term n} *}
    1.23 -text_raw{*\snip{isuccsdef}{0}{1}{% *}
    1.24 -definition
    1.25 -  "isuccs i n \<equiv> case i of 
    1.26 -     JMP j \<Rightarrow> {n + 1 + j}
    1.27 -   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
    1.28 -   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    1.29 -   | _ \<Rightarrow> {n +1}"
    1.30 -text_raw{*}%endsnip*}
    1.31 -
    1.32 -text {* The possible successors PCs of an instruction list *}
    1.33 -definition
    1.34 -  succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
    1.35 -  "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" 
    1.36 -
    1.37 -text {* Possible exit PCs of a program *}
    1.38 -definition
    1.39 -  "exits P = succs P 0 - {0..< size P}"
    1.40 -
    1.41 -  
    1.42 -subsection {* Basic properties of @{term exec_n} *}
    1.43 -
    1.44 -lemma exec_n_exec:
    1.45 -  "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
    1.46 -  by (induct n arbitrary: c) (auto simp del: exec1_def)
    1.47 -
    1.48 -lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
    1.49 -
    1.50 -lemma exec_Suc:
    1.51 -  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
    1.52 -  by (fastforce simp del: split_paired_Ex)
    1.53 -
    1.54 -lemma exec_exec_n:
    1.55 -  "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
    1.56 -  by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc)
    1.57 -    
    1.58 -lemma exec_eq_exec_n:
    1.59 -  "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
    1.60 -  by (blast intro: exec_exec_n exec_n_exec)
    1.61 -
    1.62 -lemma exec_n_Nil [simp]:
    1.63 -  "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
    1.64 -  by (induct k) auto
    1.65 -
    1.66 -lemma exec1_exec_n [intro!]:
    1.67 -  "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
    1.68 -  by (cases c') simp
    1.69 -
    1.70 -
    1.71 -subsection {* Concrete symbolic execution steps *}
    1.72 -
    1.73 -lemma exec_n_step:
    1.74 -  "n \<noteq> n' \<Longrightarrow> 
    1.75 -  P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') = 
    1.76 -  (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
    1.77 -  by (cases k) auto
    1.78 -
    1.79 -lemma exec1_end:
    1.80 -  "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
    1.81 -  by auto
    1.82 -
    1.83 -lemma exec_n_end:
    1.84 -  "size P <= (n::int) \<Longrightarrow> 
    1.85 -  P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
    1.86 -  by (cases k) (auto simp: exec1_end)
    1.87 -
    1.88 -lemmas exec_n_simps = exec_n_step exec_n_end
    1.89 -
    1.90 -
    1.91 -subsection {* Basic properties of @{term succs} *}
    1.92 -
    1.93 -lemma succs_simps [simp]: 
    1.94 -  "succs [ADD] n = {n + 1}"
    1.95 -  "succs [LOADI v] n = {n + 1}"
    1.96 -  "succs [LOAD x] n = {n + 1}"
    1.97 -  "succs [STORE x] n = {n + 1}"
    1.98 -  "succs [JMP i] n = {n + 1 + i}"
    1.99 -  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
   1.100 -  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
   1.101 -  by (auto simp: succs_def isuccs_def)
   1.102 -
   1.103 -lemma succs_empty [iff]: "succs [] n = {}"
   1.104 -  by (simp add: succs_def)
   1.105 -
   1.106 -lemma succs_Cons:
   1.107 -  "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
   1.108 -proof 
   1.109 -  let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
   1.110 -  { fix p assume "p \<in> succs (x#xs) n"
   1.111 -    then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
   1.112 -      unfolding succs_def by auto     
   1.113 -    have "p \<in> ?x \<union> ?xs" 
   1.114 -    proof cases
   1.115 -      assume "i = 0" with isuccs show ?thesis by simp
   1.116 -    next
   1.117 -      assume "i \<noteq> 0" 
   1.118 -      with isuccs 
   1.119 -      have "?isuccs p xs (1+n) (i - 1)" by auto
   1.120 -      hence "p \<in> ?xs" unfolding succs_def by blast
   1.121 -      thus ?thesis .. 
   1.122 -    qed
   1.123 -  } 
   1.124 -  thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
   1.125 -  
   1.126 -  { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
   1.127 -    hence "p \<in> succs (x#xs) n"
   1.128 -    proof
   1.129 -      assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
   1.130 -    next
   1.131 -      assume "p \<in> ?xs"
   1.132 -      then obtain i where "?isuccs p xs (1+n) i"
   1.133 -        unfolding succs_def by auto
   1.134 -      hence "?isuccs p (x#xs) n (1+i)"
   1.135 -        by (simp add: algebra_simps)
   1.136 -      thus ?thesis unfolding succs_def by blast
   1.137 -    qed
   1.138 -  }  
   1.139 -  thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
   1.140 -qed
   1.141 -
   1.142 -lemma succs_iexec1:
   1.143 -  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
   1.144 -  shows "fst c' \<in> succs P 0"
   1.145 -  using assms by (auto simp: succs_def isuccs_def split: instr.split)
   1.146 -
   1.147 -lemma succs_shift:
   1.148 -  "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
   1.149 -  by (fastforce simp: succs_def isuccs_def split: instr.split)
   1.150 -  
   1.151 -lemma inj_op_plus [simp]:
   1.152 -  "inj (op + (i::int))"
   1.153 -  by (metis add_minus_cancel inj_on_inverseI)
   1.154 -
   1.155 -lemma succs_set_shift [simp]:
   1.156 -  "op + i ` succs xs 0 = succs xs i"
   1.157 -  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)
   1.158 -
   1.159 -lemma succs_append [simp]:
   1.160 -  "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
   1.161 -  by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)
   1.162 -
   1.163 -
   1.164 -lemma exits_append [simp]:
   1.165 -  "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys - 
   1.166 -                     {0..<size xs + size ys}" 
   1.167 -  by (auto simp: exits_def image_set_diff)
   1.168 -  
   1.169 -lemma exits_single:
   1.170 -  "exits [x] = isuccs x 0 - {0}"
   1.171 -  by (auto simp: exits_def succs_def)
   1.172 -  
   1.173 -lemma exits_Cons:
   1.174 -  "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - 
   1.175 -                     {0..<1 + size xs}" 
   1.176 -  using exits_append [of "[x]" xs]
   1.177 -  by (simp add: exits_single)
   1.178 -
   1.179 -lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)
   1.180 -
   1.181 -lemma exits_simps [simp]:
   1.182 -  "exits [ADD] = {1}"
   1.183 -  "exits [LOADI v] = {1}"
   1.184 -  "exits [LOAD x] = {1}"
   1.185 -  "exits [STORE x] = {1}"
   1.186 -  "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
   1.187 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
   1.188 -  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
   1.189 -  by (auto simp: exits_def)
   1.190 -
   1.191 -lemma acomp_succs [simp]:
   1.192 -  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
   1.193 -  by (induct a arbitrary: n) auto
   1.194 -
   1.195 -lemma acomp_size:
   1.196 -  "(1::int) \<le> size (acomp a)"
   1.197 -  by (induct a) auto
   1.198 -
   1.199 -lemma acomp_exits [simp]:
   1.200 -  "exits (acomp a) = {size (acomp a)}"
   1.201 -  by (auto simp: exits_def acomp_size)
   1.202 -
   1.203 -lemma bcomp_succs:
   1.204 -  "0 \<le> i \<Longrightarrow>
   1.205 -  succs (bcomp b c i) n \<subseteq> {n .. n + size (bcomp b c i)}
   1.206 -                           \<union> {n + i + size (bcomp b c i)}" 
   1.207 -proof (induction b arbitrary: c i n)
   1.208 -  case (And b1 b2)
   1.209 -  from And.prems
   1.210 -  show ?case 
   1.211 -    by (cases c)
   1.212 -       (auto dest: And.IH(1) [THEN subsetD, rotated] 
   1.213 -                   And.IH(2) [THEN subsetD, rotated])
   1.214 -qed auto
   1.215 -
   1.216 -lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
   1.217 -
   1.218 -lemma bcomp_exits:
   1.219 -  fixes i :: int
   1.220 -  shows
   1.221 -  "0 \<le> i \<Longrightarrow>
   1.222 -  exits (bcomp b c i) \<subseteq> {size (bcomp b c i), i + size (bcomp b c i)}" 
   1.223 -  by (auto simp: exits_def)
   1.224 -  
   1.225 -lemma bcomp_exitsD [dest!]:
   1.226 -  "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow> 
   1.227 -  p = size (bcomp b c i) \<or> p = i + size (bcomp b c i)"
   1.228 -  using bcomp_exits by auto
   1.229 -
   1.230 -lemma ccomp_succs:
   1.231 -  "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}"
   1.232 -proof (induction c arbitrary: n)
   1.233 -  case SKIP thus ?case by simp
   1.234 -next
   1.235 -  case Assign thus ?case by simp
   1.236 -next
   1.237 -  case (Seq c1 c2)
   1.238 -  from Seq.prems
   1.239 -  show ?case 
   1.240 -    by (fastforce dest: Seq.IH [THEN subsetD])
   1.241 -next
   1.242 -  case (If b c1 c2)
   1.243 -  from If.prems
   1.244 -  show ?case
   1.245 -    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
   1.246 -next
   1.247 -  case (While b c)
   1.248 -  from While.prems
   1.249 -  show ?case by (auto dest!: While.IH [THEN subsetD])
   1.250 -qed
   1.251 -
   1.252 -lemma ccomp_exits:
   1.253 -  "exits (ccomp c) \<subseteq> {size (ccomp c)}"
   1.254 -  using ccomp_succs [of c 0] by (auto simp: exits_def)
   1.255 -
   1.256 -lemma ccomp_exitsD [dest!]:
   1.257 -  "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)"
   1.258 -  using ccomp_exits by auto
   1.259 -
   1.260 -
   1.261 -subsection {* Splitting up machine executions *}
   1.262 -
   1.263 -lemma exec1_split:
   1.264 -  fixes i j :: int
   1.265 -  shows
   1.266 -  "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> 
   1.267 -  c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
   1.268 -  by (auto split: instr.splits)
   1.269 -
   1.270 -lemma exec_n_split:
   1.271 -  fixes i j :: int
   1.272 -  assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
   1.273 -          "0 \<le> i" "i < size c" 
   1.274 -          "j \<notin> {size P ..< size P + size c}"
   1.275 -  shows "\<exists>s'' (i'::int) k m. 
   1.276 -                   c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
   1.277 -                   i' \<in> exits c \<and> 
   1.278 -                   P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and>
   1.279 -                   n = k + m" 
   1.280 -using assms proof (induction n arbitrary: i j s)
   1.281 -  case 0
   1.282 -  thus ?case by simp
   1.283 -next
   1.284 -  case (Suc n)
   1.285 -  have i: "0 \<le> i" "i < size c" by fact+
   1.286 -  from Suc.prems
   1.287 -  have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp
   1.288 -  from Suc.prems 
   1.289 -  obtain i0 s0 where
   1.290 -    step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and
   1.291 -    rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
   1.292 -    by clarsimp
   1.293 -
   1.294 -  from step i
   1.295 -  have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split)
   1.296 -
   1.297 -  have "i0 = size P + (i0 - size P) " by simp
   1.298 -  then obtain j0::int where j0: "i0 = size P + j0"  ..
   1.299 -
   1.300 -  note split_paired_Ex [simp del]
   1.301 -
   1.302 -  { assume "j0 \<in> {0 ..< size c}"
   1.303 -    with j0 j rest c
   1.304 -    have ?case
   1.305 -      by (fastforce dest!: Suc.IH intro!: exec_Suc)
   1.306 -  } moreover {
   1.307 -    assume "j0 \<notin> {0 ..< size c}"
   1.308 -    moreover
   1.309 -    from c j0 have "j0 \<in> succs c 0"
   1.310 -      by (auto dest: succs_iexec1 simp del: iexec.simps)
   1.311 -    ultimately
   1.312 -    have "j0 \<in> exits c" by (simp add: exits_def)
   1.313 -    with c j0 rest
   1.314 -    have ?case by fastforce
   1.315 -  }
   1.316 -  ultimately
   1.317 -  show ?case by cases
   1.318 -qed
   1.319 -
   1.320 -lemma exec_n_drop_right:
   1.321 -  fixes j :: int
   1.322 -  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}"
   1.323 -  shows "\<exists>s'' i' k m. 
   1.324 -          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
   1.325 -           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
   1.326 -           i' \<in> exits c) \<and> 
   1.327 -           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
   1.328 -           n = k + m"
   1.329 -  using assms
   1.330 -  by (cases "c = []")
   1.331 -     (auto dest: exec_n_split [where P="[]", simplified])
   1.332 -  
   1.333 -
   1.334 -text {*
   1.335 -  Dropping the left context of a potentially incomplete execution of @{term c}.
   1.336 -*}
   1.337 -
   1.338 -lemma exec1_drop_left:
   1.339 -  fixes i n :: int
   1.340 -  assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i"
   1.341 -  shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')"
   1.342 -proof -
   1.343 -  have "i = size P1 + (i - size P1)" by simp 
   1.344 -  then obtain i' :: int where "i = size P1 + i'" ..
   1.345 -  moreover
   1.346 -  have "n = size P1 + (n - size P1)" by simp 
   1.347 -  then obtain n' :: int where "n = size P1 + n'" ..
   1.348 -  ultimately 
   1.349 -  show ?thesis using assms by (clarsimp simp del: iexec.simps)
   1.350 -qed
   1.351 -
   1.352 -lemma exec_n_drop_left:
   1.353 -  fixes i n :: int
   1.354 -  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
   1.355 -          "size P \<le> i" "exits P' \<subseteq> {0..}"
   1.356 -  shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')"
   1.357 -using assms proof (induction k arbitrary: i s stk)
   1.358 -  case 0 thus ?case by simp
   1.359 -next
   1.360 -  case (Suc k)
   1.361 -  from Suc.prems
   1.362 -  obtain i' s'' stk'' where
   1.363 -    step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
   1.364 -    rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
   1.365 -    by (auto simp del: exec1_def)
   1.366 -  from step `size P \<le> i`
   1.367 -  have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
   1.368 -    by (rule exec1_drop_left)
   1.369 -  moreover
   1.370 -  then have "i' - size P \<in> succs P' 0"
   1.371 -    by (fastforce dest!: succs_iexec1 simp del: iexec.simps)
   1.372 -  with `exits P' \<subseteq> {0..}`
   1.373 -  have "size P \<le> i'" by (auto simp: exits_def)
   1.374 -  from rest this `exits P' \<subseteq> {0..}`     
   1.375 -  have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
   1.376 -    by (rule Suc.IH)
   1.377 -  ultimately
   1.378 -  show ?case by auto
   1.379 -qed
   1.380 -
   1.381 -lemmas exec_n_drop_Cons = 
   1.382 -  exec_n_drop_left [where P="[instr]", simplified] for instr
   1.383 -
   1.384 -definition
   1.385 -  "closed P \<longleftrightarrow> exits P \<subseteq> {size P}" 
   1.386 -
   1.387 -lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
   1.388 -  using ccomp_exits by (auto simp: closed_def)
   1.389 -
   1.390 -lemma acomp_closed [simp, intro!]: "closed (acomp c)"
   1.391 -  by (simp add: closed_def)
   1.392 -
   1.393 -lemma exec_n_split_full:
   1.394 -  fixes j :: int
   1.395 -  assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
   1.396 -  assumes P: "size P \<le> j" 
   1.397 -  assumes closed: "closed P"
   1.398 -  assumes exits: "exits P' \<subseteq> {0..}"
   1.399 -  shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and> 
   1.400 -                           P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')"
   1.401 -proof (cases "P")
   1.402 -  case Nil with exec
   1.403 -  show ?thesis by fastforce
   1.404 -next
   1.405 -  case Cons
   1.406 -  hence "0 < size P" by simp
   1.407 -  with exec P closed
   1.408 -  obtain k1 k2 s'' stk'' where
   1.409 -    1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and
   1.410 -    2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
   1.411 -    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] 
   1.412 -             simp: closed_def)
   1.413 -  moreover
   1.414 -  have "j = size P + (j - size P)" by simp
   1.415 -  then obtain j0 :: int where "j = size P + j0" ..
   1.416 -  ultimately
   1.417 -  show ?thesis using exits
   1.418 -    by (fastforce dest: exec_n_drop_left)
   1.419 -qed
   1.420 -
   1.421 -
   1.422 -subsection {* Correctness theorem *}
   1.423 -
   1.424 -lemma acomp_neq_Nil [simp]:
   1.425 -  "acomp a \<noteq> []"
   1.426 -  by (induct a) auto
   1.427 -
   1.428 -lemma acomp_exec_n [dest!]:
   1.429 -  "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow> 
   1.430 -  s' = s \<and> stk' = aval a s#stk"
   1.431 -proof (induction a arbitrary: n s' stk stk')
   1.432 -  case (Plus a1 a2)
   1.433 -  let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
   1.434 -  from Plus.prems
   1.435 -  have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" 
   1.436 -    by (simp add: algebra_simps)
   1.437 -      
   1.438 -  then obtain n1 s1 stk1 n2 s2 stk2 n3 where 
   1.439 -    "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
   1.440 -    "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" 
   1.441 -       "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
   1.442 -    by (auto dest!: exec_n_split_full)
   1.443 -
   1.444 -  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
   1.445 -qed (auto simp: exec_n_simps)
   1.446 -
   1.447 -lemma bcomp_split:
   1.448 -  fixes i j :: int
   1.449 -  assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
   1.450 -          "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i"
   1.451 -  shows "\<exists>s'' stk'' (i'::int) k m. 
   1.452 -           bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
   1.453 -           (i' = size (bcomp b c i) \<or> i' = i + size (bcomp b c i)) \<and>
   1.454 -           bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
   1.455 -           n = k + m"
   1.456 -  using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+
   1.457 -
   1.458 -lemma bcomp_exec_n [dest]:
   1.459 -  fixes i j :: int
   1.460 -  assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
   1.461 -          "size (bcomp b c j) \<le> i" "0 \<le> j"
   1.462 -  shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and>
   1.463 -         s' = s \<and> stk' = stk"
   1.464 -using assms proof (induction b arbitrary: c j i n s' stk')
   1.465 -  case Bc thus ?case 
   1.466 -    by (simp split: split_if_asm add: exec_n_simps)
   1.467 -next
   1.468 -  case (Not b) 
   1.469 -  from Not.prems show ?case
   1.470 -    by (fastforce dest!: Not.IH) 
   1.471 -next
   1.472 -  case (And b1 b2)
   1.473 -  
   1.474 -  let ?b2 = "bcomp b2 c j" 
   1.475 -  let ?m  = "if c then size ?b2 else size ?b2 + j"
   1.476 -  let ?b1 = "bcomp b1 False ?m" 
   1.477 -
   1.478 -  have j: "size (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+
   1.479 -  
   1.480 -  from And.prems
   1.481 -  obtain s'' stk'' and i'::int and k m where 
   1.482 -    b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')"
   1.483 -        "i' = size ?b1 \<or> i' = ?m + size ?b1" and
   1.484 -    b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')"
   1.485 -    by (auto dest!: bcomp_split dest: exec_n_drop_left)
   1.486 -  from b1 j
   1.487 -  have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
   1.488 -    by (auto dest!: And.IH)
   1.489 -  with b2 j
   1.490 -  show ?case 
   1.491 -    by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
   1.492 -next
   1.493 -  case Less
   1.494 -  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
   1.495 -qed
   1.496 -
   1.497 -lemma ccomp_empty [elim!]:
   1.498 -  "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
   1.499 -  by (induct c) auto
   1.500 -
   1.501 -declare assign_simp [simp]
   1.502 -
   1.503 -lemma ccomp_exec_n:
   1.504 -  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk')
   1.505 -  \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
   1.506 -proof (induction c arbitrary: s t stk stk' n)
   1.507 -  case SKIP
   1.508 -  thus ?case by auto
   1.509 -next
   1.510 -  case (Assign x a)
   1.511 -  thus ?case
   1.512 -    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
   1.513 -next
   1.514 -  case (Seq c1 c2)
   1.515 -  thus ?case by (fastforce dest!: exec_n_split_full)
   1.516 -next
   1.517 -  case (If b c1 c2)
   1.518 -  note If.IH [dest!]
   1.519 -
   1.520 -  let ?if = "IF b THEN c1 ELSE c2"
   1.521 -  let ?cs = "ccomp ?if"
   1.522 -  let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"
   1.523 -  
   1.524 -  from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')`
   1.525 -  obtain i' :: int and k m s'' stk'' where
   1.526 -    cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and
   1.527 -        "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" 
   1.528 -        "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1"
   1.529 -    by (auto dest!: bcomp_split)
   1.530 -
   1.531 -  hence i':
   1.532 -    "s''=s" "stk'' = stk" 
   1.533 -    "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
   1.534 -    by auto
   1.535 -  
   1.536 -  with cs have cs':
   1.537 -    "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile> 
   1.538 -       (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m
   1.539 -       (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
   1.540 -    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
   1.541 -     
   1.542 -  show ?case
   1.543 -  proof (cases "bval b s")
   1.544 -    case True with cs'
   1.545 -    show ?thesis
   1.546 -      by simp
   1.547 -         (fastforce dest: exec_n_drop_right 
   1.548 -                   split: split_if_asm simp: exec_n_simps)
   1.549 -  next
   1.550 -    case False with cs'
   1.551 -    show ?thesis
   1.552 -      by (auto dest!: exec_n_drop_Cons exec_n_drop_left 
   1.553 -               simp: exits_Cons isuccs_def)
   1.554 -  qed
   1.555 -next
   1.556 -  case (While b c)
   1.557 -
   1.558 -  from While.prems
   1.559 -  show ?case
   1.560 -  proof (induction n arbitrary: s rule: nat_less_induct)
   1.561 -    case (1 n)
   1.562 -    
   1.563 -    { assume "\<not> bval b s"
   1.564 -      with "1.prems"
   1.565 -      have ?case
   1.566 -        by simp
   1.567 -           (fastforce dest!: bcomp_exec_n bcomp_split 
   1.568 -                     simp: exec_n_simps)
   1.569 -    } moreover {
   1.570 -      assume b: "bval b s"
   1.571 -      let ?c0 = "WHILE b DO c"
   1.572 -      let ?cs = "ccomp ?c0"
   1.573 -      let ?bs = "bcomp b False (size (ccomp c) + 1)"
   1.574 -      let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"
   1.575 -      
   1.576 -      from "1.prems" b
   1.577 -      obtain k where
   1.578 -        cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and
   1.579 -        k:  "k \<le> n"
   1.580 -        by (fastforce dest!: bcomp_split)
   1.581 -      
   1.582 -      have ?case
   1.583 -      proof cases
   1.584 -        assume "ccomp c = []"
   1.585 -        with cs k
   1.586 -        obtain m where
   1.587 -          "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
   1.588 -          "m < n"
   1.589 -          by (auto simp: exec_n_step [where k=k])
   1.590 -        with "1.IH"
   1.591 -        show ?case by blast
   1.592 -      next
   1.593 -        assume "ccomp c \<noteq> []"
   1.594 -        with cs
   1.595 -        obtain m m' s'' stk'' where
   1.596 -          c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and 
   1.597 -          rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m 
   1.598 -                       (size ?cs, t, stk')" and
   1.599 -          m: "k = m + m'"
   1.600 -          by (auto dest: exec_n_split [where i=0, simplified])
   1.601 -        from c
   1.602 -        have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
   1.603 -          by (auto dest!: While.IH)
   1.604 -        moreover
   1.605 -        from rest m k stk
   1.606 -        obtain k' where
   1.607 -          "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
   1.608 -          "k' < n"
   1.609 -          by (auto simp: exec_n_step [where k=m])
   1.610 -        with "1.IH"
   1.611 -        have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
   1.612 -        ultimately
   1.613 -        show ?case using b by blast
   1.614 -      qed
   1.615 -    }
   1.616 -    ultimately show ?case by cases
   1.617 -  qed
   1.618 -qed
   1.619 -
   1.620 -theorem ccomp_exec:
   1.621 -  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
   1.622 -  by (auto dest: exec_exec_n ccomp_exec_n)
   1.623 -
   1.624 -corollary ccomp_sound:
   1.625 -  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)  \<longleftrightarrow>  (c,s) \<Rightarrow> t"
   1.626 -  by (blast intro!: ccomp_exec ccomp_bigstep)
   1.627 -
   1.628 -end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/Compiler2.thy	Thu Jun 20 17:26:16 2013 +0200
     2.3 @@ -0,0 +1,625 @@
     2.4 +(* Author: Gerwin Klein *)
     2.5 +
     2.6 +theory Compiler2
     2.7 +imports Compiler
     2.8 +begin
     2.9 +
    2.10 +section {* Compiler Correctness, Reverse Direction *}
    2.11 +
    2.12 +subsection {* Definitions *}
    2.13 +
    2.14 +text {* Execution in @{term n} steps for simpler induction *}
    2.15 +primrec 
    2.16 +  exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" 
    2.17 +  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
    2.18 +where 
    2.19 +  "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
    2.20 +  "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"
    2.21 +
    2.22 +text {* The possible successor PCs of an instruction at position @{term n} *}
    2.23 +text_raw{*\snip{isuccsdef}{0}{1}{% *}
    2.24 +definition
    2.25 +  "isuccs i n \<equiv> case i of 
    2.26 +     JMP j \<Rightarrow> {n + 1 + j}
    2.27 +   | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1}
    2.28 +   | JMPGE j \<Rightarrow> {n + 1 + j, n + 1}
    2.29 +   | _ \<Rightarrow> {n +1}"
    2.30 +text_raw{*}%endsnip*}
    2.31 +
    2.32 +text {* The possible successors PCs of an instruction list *}
    2.33 +definition
    2.34 +  succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
    2.35 +  "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" 
    2.36 +
    2.37 +text {* Possible exit PCs of a program *}
    2.38 +definition
    2.39 +  "exits P = succs P 0 - {0..< size P}"
    2.40 +
    2.41 +  
    2.42 +subsection {* Basic properties of @{term exec_n} *}
    2.43 +
    2.44 +lemma exec_n_exec:
    2.45 +  "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
    2.46 +  by (induct n arbitrary: c) (auto simp del: exec1_def)
    2.47 +
    2.48 +lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
    2.49 +
    2.50 +lemma exec_Suc:
    2.51 +  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" 
    2.52 +  by (fastforce simp del: split_paired_Ex)
    2.53 +
    2.54 +lemma exec_exec_n:
    2.55 +  "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
    2.56 +  by (induct rule: exec.induct) (auto simp del: exec1_def intro: exec_Suc)
    2.57 +    
    2.58 +lemma exec_eq_exec_n:
    2.59 +  "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
    2.60 +  by (blast intro: exec_exec_n exec_n_exec)
    2.61 +
    2.62 +lemma exec_n_Nil [simp]:
    2.63 +  "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
    2.64 +  by (induct k) auto
    2.65 +
    2.66 +lemma exec1_exec_n [intro!]:
    2.67 +  "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
    2.68 +  by (cases c') simp
    2.69 +
    2.70 +
    2.71 +subsection {* Concrete symbolic execution steps *}
    2.72 +
    2.73 +lemma exec_n_step:
    2.74 +  "n \<noteq> n' \<Longrightarrow> 
    2.75 +  P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') = 
    2.76 +  (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
    2.77 +  by (cases k) auto
    2.78 +
    2.79 +lemma exec1_end:
    2.80 +  "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
    2.81 +  by auto
    2.82 +
    2.83 +lemma exec_n_end:
    2.84 +  "size P <= (n::int) \<Longrightarrow> 
    2.85 +  P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
    2.86 +  by (cases k) (auto simp: exec1_end)
    2.87 +
    2.88 +lemmas exec_n_simps = exec_n_step exec_n_end
    2.89 +
    2.90 +
    2.91 +subsection {* Basic properties of @{term succs} *}
    2.92 +
    2.93 +lemma succs_simps [simp]: 
    2.94 +  "succs [ADD] n = {n + 1}"
    2.95 +  "succs [LOADI v] n = {n + 1}"
    2.96 +  "succs [LOAD x] n = {n + 1}"
    2.97 +  "succs [STORE x] n = {n + 1}"
    2.98 +  "succs [JMP i] n = {n + 1 + i}"
    2.99 +  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
   2.100 +  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
   2.101 +  by (auto simp: succs_def isuccs_def)
   2.102 +
   2.103 +lemma succs_empty [iff]: "succs [] n = {}"
   2.104 +  by (simp add: succs_def)
   2.105 +
   2.106 +lemma succs_Cons:
   2.107 +  "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
   2.108 +proof 
   2.109 +  let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
   2.110 +  { fix p assume "p \<in> succs (x#xs) n"
   2.111 +    then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
   2.112 +      unfolding succs_def by auto     
   2.113 +    have "p \<in> ?x \<union> ?xs" 
   2.114 +    proof cases
   2.115 +      assume "i = 0" with isuccs show ?thesis by simp
   2.116 +    next
   2.117 +      assume "i \<noteq> 0" 
   2.118 +      with isuccs 
   2.119 +      have "?isuccs p xs (1+n) (i - 1)" by auto
   2.120 +      hence "p \<in> ?xs" unfolding succs_def by blast
   2.121 +      thus ?thesis .. 
   2.122 +    qed
   2.123 +  } 
   2.124 +  thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
   2.125 +  
   2.126 +  { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
   2.127 +    hence "p \<in> succs (x#xs) n"
   2.128 +    proof
   2.129 +      assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
   2.130 +    next
   2.131 +      assume "p \<in> ?xs"
   2.132 +      then obtain i where "?isuccs p xs (1+n) i"
   2.133 +        unfolding succs_def by auto
   2.134 +      hence "?isuccs p (x#xs) n (1+i)"
   2.135 +        by (simp add: algebra_simps)
   2.136 +      thus ?thesis unfolding succs_def by blast
   2.137 +    qed
   2.138 +  }  
   2.139 +  thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
   2.140 +qed
   2.141 +
   2.142 +lemma succs_iexec1:
   2.143 +  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
   2.144 +  shows "fst c' \<in> succs P 0"
   2.145 +  using assms by (auto simp: succs_def isuccs_def split: instr.split)
   2.146 +
   2.147 +lemma succs_shift:
   2.148 +  "(p - n \<in> succs P 0) = (p \<in> succs P n)" 
   2.149 +  by (fastforce simp: succs_def isuccs_def split: instr.split)
   2.150 +  
   2.151 +lemma inj_op_plus [simp]:
   2.152 +  "inj (op + (i::int))"
   2.153 +  by (metis add_minus_cancel inj_on_inverseI)
   2.154 +
   2.155 +lemma succs_set_shift [simp]:
   2.156 +  "op + i ` succs xs 0 = succs xs i"
   2.157 +  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)
   2.158 +
   2.159 +lemma succs_append [simp]:
   2.160 +  "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
   2.161 +  by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)
   2.162 +
   2.163 +
   2.164 +lemma exits_append [simp]:
   2.165 +  "exits (xs @ ys) = exits xs \<union> (op + (size xs)) ` exits ys - 
   2.166 +                     {0..<size xs + size ys}" 
   2.167 +  by (auto simp: exits_def image_set_diff)
   2.168 +  
   2.169 +lemma exits_single:
   2.170 +  "exits [x] = isuccs x 0 - {0}"
   2.171 +  by (auto simp: exits_def succs_def)
   2.172 +  
   2.173 +lemma exits_Cons:
   2.174 +  "exits (x # xs) = (isuccs x 0 - {0}) \<union> (op + 1) ` exits xs - 
   2.175 +                     {0..<1 + size xs}" 
   2.176 +  using exits_append [of "[x]" xs]
   2.177 +  by (simp add: exits_single)
   2.178 +
   2.179 +lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)
   2.180 +
   2.181 +lemma exits_simps [simp]:
   2.182 +  "exits [ADD] = {1}"
   2.183 +  "exits [LOADI v] = {1}"
   2.184 +  "exits [LOAD x] = {1}"
   2.185 +  "exits [STORE x] = {1}"
   2.186 +  "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
   2.187 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
   2.188 +  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
   2.189 +  by (auto simp: exits_def)
   2.190 +
   2.191 +lemma acomp_succs [simp]:
   2.192 +  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
   2.193 +  by (induct a arbitrary: n) auto
   2.194 +
   2.195 +lemma acomp_size:
   2.196 +  "(1::int) \<le> size (acomp a)"
   2.197 +  by (induct a) auto
   2.198 +
   2.199 +lemma acomp_exits [simp]:
   2.200 +  "exits (acomp a) = {size (acomp a)}"
   2.201 +  by (auto simp: exits_def acomp_size)
   2.202 +
   2.203 +lemma bcomp_succs:
   2.204 +  "0 \<le> i \<Longrightarrow>
   2.205 +  succs (bcomp b c i) n \<subseteq> {n .. n + size (bcomp b c i)}
   2.206 +                           \<union> {n + i + size (bcomp b c i)}" 
   2.207 +proof (induction b arbitrary: c i n)
   2.208 +  case (And b1 b2)
   2.209 +  from And.prems
   2.210 +  show ?case 
   2.211 +    by (cases c)
   2.212 +       (auto dest: And.IH(1) [THEN subsetD, rotated] 
   2.213 +                   And.IH(2) [THEN subsetD, rotated])
   2.214 +qed auto
   2.215 +
   2.216 +lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
   2.217 +
   2.218 +lemma bcomp_exits:
   2.219 +  fixes i :: int
   2.220 +  shows
   2.221 +  "0 \<le> i \<Longrightarrow>
   2.222 +  exits (bcomp b c i) \<subseteq> {size (bcomp b c i), i + size (bcomp b c i)}" 
   2.223 +  by (auto simp: exits_def)
   2.224 +  
   2.225 +lemma bcomp_exitsD [dest!]:
   2.226 +  "p \<in> exits (bcomp b c i) \<Longrightarrow> 0 \<le> i \<Longrightarrow> 
   2.227 +  p = size (bcomp b c i) \<or> p = i + size (bcomp b c i)"
   2.228 +  using bcomp_exits by auto
   2.229 +
   2.230 +lemma ccomp_succs:
   2.231 +  "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}"
   2.232 +proof (induction c arbitrary: n)
   2.233 +  case SKIP thus ?case by simp
   2.234 +next
   2.235 +  case Assign thus ?case by simp
   2.236 +next
   2.237 +  case (Seq c1 c2)
   2.238 +  from Seq.prems
   2.239 +  show ?case 
   2.240 +    by (fastforce dest: Seq.IH [THEN subsetD])
   2.241 +next
   2.242 +  case (If b c1 c2)
   2.243 +  from If.prems
   2.244 +  show ?case
   2.245 +    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
   2.246 +next
   2.247 +  case (While b c)
   2.248 +  from While.prems
   2.249 +  show ?case by (auto dest!: While.IH [THEN subsetD])
   2.250 +qed
   2.251 +
   2.252 +lemma ccomp_exits:
   2.253 +  "exits (ccomp c) \<subseteq> {size (ccomp c)}"
   2.254 +  using ccomp_succs [of c 0] by (auto simp: exits_def)
   2.255 +
   2.256 +lemma ccomp_exitsD [dest!]:
   2.257 +  "p \<in> exits (ccomp c) \<Longrightarrow> p = size (ccomp c)"
   2.258 +  using ccomp_exits by auto
   2.259 +
   2.260 +
   2.261 +subsection {* Splitting up machine executions *}
   2.262 +
   2.263 +lemma exec1_split:
   2.264 +  fixes i j :: int
   2.265 +  shows
   2.266 +  "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow> 
   2.267 +  c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
   2.268 +  by (auto split: instr.splits)
   2.269 +
   2.270 +lemma exec_n_split:
   2.271 +  fixes i j :: int
   2.272 +  assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
   2.273 +          "0 \<le> i" "i < size c" 
   2.274 +          "j \<notin> {size P ..< size P + size c}"
   2.275 +  shows "\<exists>s'' (i'::int) k m. 
   2.276 +                   c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
   2.277 +                   i' \<in> exits c \<and> 
   2.278 +                   P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and>
   2.279 +                   n = k + m" 
   2.280 +using assms proof (induction n arbitrary: i j s)
   2.281 +  case 0
   2.282 +  thus ?case by simp
   2.283 +next
   2.284 +  case (Suc n)
   2.285 +  have i: "0 \<le> i" "i < size c" by fact+
   2.286 +  from Suc.prems
   2.287 +  have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp
   2.288 +  from Suc.prems 
   2.289 +  obtain i0 s0 where
   2.290 +    step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and
   2.291 +    rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
   2.292 +    by clarsimp
   2.293 +
   2.294 +  from step i
   2.295 +  have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by (rule exec1_split)
   2.296 +
   2.297 +  have "i0 = size P + (i0 - size P) " by simp
   2.298 +  then obtain j0::int where j0: "i0 = size P + j0"  ..
   2.299 +
   2.300 +  note split_paired_Ex [simp del]
   2.301 +
   2.302 +  { assume "j0 \<in> {0 ..< size c}"
   2.303 +    with j0 j rest c
   2.304 +    have ?case
   2.305 +      by (fastforce dest!: Suc.IH intro!: exec_Suc)
   2.306 +  } moreover {
   2.307 +    assume "j0 \<notin> {0 ..< size c}"
   2.308 +    moreover
   2.309 +    from c j0 have "j0 \<in> succs c 0"
   2.310 +      by (auto dest: succs_iexec1 simp del: iexec.simps)
   2.311 +    ultimately
   2.312 +    have "j0 \<in> exits c" by (simp add: exits_def)
   2.313 +    with c j0 rest
   2.314 +    have ?case by fastforce
   2.315 +  }
   2.316 +  ultimately
   2.317 +  show ?case by cases
   2.318 +qed
   2.319 +
   2.320 +lemma exec_n_drop_right:
   2.321 +  fixes j :: int
   2.322 +  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}"
   2.323 +  shows "\<exists>s'' i' k m. 
   2.324 +          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
   2.325 +           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
   2.326 +           i' \<in> exits c) \<and> 
   2.327 +           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
   2.328 +           n = k + m"
   2.329 +  using assms
   2.330 +  by (cases "c = []")
   2.331 +     (auto dest: exec_n_split [where P="[]", simplified])
   2.332 +  
   2.333 +
   2.334 +text {*
   2.335 +  Dropping the left context of a potentially incomplete execution of @{term c}.
   2.336 +*}
   2.337 +
   2.338 +lemma exec1_drop_left:
   2.339 +  fixes i n :: int
   2.340 +  assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i"
   2.341 +  shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')"
   2.342 +proof -
   2.343 +  have "i = size P1 + (i - size P1)" by simp 
   2.344 +  then obtain i' :: int where "i = size P1 + i'" ..
   2.345 +  moreover
   2.346 +  have "n = size P1 + (n - size P1)" by simp 
   2.347 +  then obtain n' :: int where "n = size P1 + n'" ..
   2.348 +  ultimately 
   2.349 +  show ?thesis using assms by (clarsimp simp del: iexec.simps)
   2.350 +qed
   2.351 +
   2.352 +lemma exec_n_drop_left:
   2.353 +  fixes i n :: int
   2.354 +  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
   2.355 +          "size P \<le> i" "exits P' \<subseteq> {0..}"
   2.356 +  shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')"
   2.357 +using assms proof (induction k arbitrary: i s stk)
   2.358 +  case 0 thus ?case by simp
   2.359 +next
   2.360 +  case (Suc k)
   2.361 +  from Suc.prems
   2.362 +  obtain i' s'' stk'' where
   2.363 +    step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
   2.364 +    rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
   2.365 +    by (auto simp del: exec1_def)
   2.366 +  from step `size P \<le> i`
   2.367 +  have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
   2.368 +    by (rule exec1_drop_left)
   2.369 +  moreover
   2.370 +  then have "i' - size P \<in> succs P' 0"
   2.371 +    by (fastforce dest!: succs_iexec1 simp del: iexec.simps)
   2.372 +  with `exits P' \<subseteq> {0..}`
   2.373 +  have "size P \<le> i'" by (auto simp: exits_def)
   2.374 +  from rest this `exits P' \<subseteq> {0..}`     
   2.375 +  have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
   2.376 +    by (rule Suc.IH)
   2.377 +  ultimately
   2.378 +  show ?case by auto
   2.379 +qed
   2.380 +
   2.381 +lemmas exec_n_drop_Cons = 
   2.382 +  exec_n_drop_left [where P="[instr]", simplified] for instr
   2.383 +
   2.384 +definition
   2.385 +  "closed P \<longleftrightarrow> exits P \<subseteq> {size P}" 
   2.386 +
   2.387 +lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
   2.388 +  using ccomp_exits by (auto simp: closed_def)
   2.389 +
   2.390 +lemma acomp_closed [simp, intro!]: "closed (acomp c)"
   2.391 +  by (simp add: closed_def)
   2.392 +
   2.393 +lemma exec_n_split_full:
   2.394 +  fixes j :: int
   2.395 +  assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
   2.396 +  assumes P: "size P \<le> j" 
   2.397 +  assumes closed: "closed P"
   2.398 +  assumes exits: "exits P' \<subseteq> {0..}"
   2.399 +  shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and> 
   2.400 +                           P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')"
   2.401 +proof (cases "P")
   2.402 +  case Nil with exec
   2.403 +  show ?thesis by fastforce
   2.404 +next
   2.405 +  case Cons
   2.406 +  hence "0 < size P" by simp
   2.407 +  with exec P closed
   2.408 +  obtain k1 k2 s'' stk'' where
   2.409 +    1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and
   2.410 +    2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
   2.411 +    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] 
   2.412 +             simp: closed_def)
   2.413 +  moreover
   2.414 +  have "j = size P + (j - size P)" by simp
   2.415 +  then obtain j0 :: int where "j = size P + j0" ..
   2.416 +  ultimately
   2.417 +  show ?thesis using exits
   2.418 +    by (fastforce dest: exec_n_drop_left)
   2.419 +qed
   2.420 +
   2.421 +
   2.422 +subsection {* Correctness theorem *}
   2.423 +
   2.424 +lemma acomp_neq_Nil [simp]:
   2.425 +  "acomp a \<noteq> []"
   2.426 +  by (induct a) auto
   2.427 +
   2.428 +lemma acomp_exec_n [dest!]:
   2.429 +  "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow> 
   2.430 +  s' = s \<and> stk' = aval a s#stk"
   2.431 +proof (induction a arbitrary: n s' stk stk')
   2.432 +  case (Plus a1 a2)
   2.433 +  let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
   2.434 +  from Plus.prems
   2.435 +  have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (?sz, s', stk')" 
   2.436 +    by (simp add: algebra_simps)
   2.437 +      
   2.438 +  then obtain n1 s1 stk1 n2 s2 stk2 n3 where 
   2.439 +    "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
   2.440 +    "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)" 
   2.441 +       "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
   2.442 +    by (auto dest!: exec_n_split_full)
   2.443 +
   2.444 +  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps)
   2.445 +qed (auto simp: exec_n_simps)
   2.446 +
   2.447 +lemma bcomp_split:
   2.448 +  fixes i j :: int
   2.449 +  assumes "bcomp b c i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')" 
   2.450 +          "j \<notin> {0..<size (bcomp b c i)}" "0 \<le> i"
   2.451 +  shows "\<exists>s'' stk'' (i'::int) k m. 
   2.452 +           bcomp b c i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
   2.453 +           (i' = size (bcomp b c i) \<or> i' = i + size (bcomp b c i)) \<and>
   2.454 +           bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
   2.455 +           n = k + m"
   2.456 +  using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+
   2.457 +
   2.458 +lemma bcomp_exec_n [dest]:
   2.459 +  fixes i j :: int
   2.460 +  assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
   2.461 +          "size (bcomp b c j) \<le> i" "0 \<le> j"
   2.462 +  shows "i = size(bcomp b c j) + (if c = bval b s then j else 0) \<and>
   2.463 +         s' = s \<and> stk' = stk"
   2.464 +using assms proof (induction b arbitrary: c j i n s' stk')
   2.465 +  case Bc thus ?case 
   2.466 +    by (simp split: split_if_asm add: exec_n_simps)
   2.467 +next
   2.468 +  case (Not b) 
   2.469 +  from Not.prems show ?case
   2.470 +    by (fastforce dest!: Not.IH) 
   2.471 +next
   2.472 +  case (And b1 b2)
   2.473 +  
   2.474 +  let ?b2 = "bcomp b2 c j" 
   2.475 +  let ?m  = "if c then size ?b2 else size ?b2 + j"
   2.476 +  let ?b1 = "bcomp b1 False ?m" 
   2.477 +
   2.478 +  have j: "size (bcomp (And b1 b2) c j) \<le> i" "0 \<le> j" by fact+
   2.479 +  
   2.480 +  from And.prems
   2.481 +  obtain s'' stk'' and i'::int and k m where 
   2.482 +    b1: "?b1 \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'')"
   2.483 +        "i' = size ?b1 \<or> i' = ?m + size ?b1" and
   2.484 +    b2: "?b2 \<turnstile> (i' - size ?b1, s'', stk'') \<rightarrow>^m (i - size ?b1, s', stk')"
   2.485 +    by (auto dest!: bcomp_split dest: exec_n_drop_left)
   2.486 +  from b1 j
   2.487 +  have "i' = size ?b1 + (if \<not>bval b1 s then ?m else 0) \<and> s'' = s \<and> stk'' = stk"
   2.488 +    by (auto dest!: And.IH)
   2.489 +  with b2 j
   2.490 +  show ?case 
   2.491 +    by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
   2.492 +next
   2.493 +  case Less
   2.494 +  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *) 
   2.495 +qed
   2.496 +
   2.497 +lemma ccomp_empty [elim!]:
   2.498 +  "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
   2.499 +  by (induct c) auto
   2.500 +
   2.501 +declare assign_simp [simp]
   2.502 +
   2.503 +lemma ccomp_exec_n:
   2.504 +  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk')
   2.505 +  \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
   2.506 +proof (induction c arbitrary: s t stk stk' n)
   2.507 +  case SKIP
   2.508 +  thus ?case by auto
   2.509 +next
   2.510 +  case (Assign x a)
   2.511 +  thus ?case
   2.512 +    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
   2.513 +next
   2.514 +  case (Seq c1 c2)
   2.515 +  thus ?case by (fastforce dest!: exec_n_split_full)
   2.516 +next
   2.517 +  case (If b c1 c2)
   2.518 +  note If.IH [dest!]
   2.519 +
   2.520 +  let ?if = "IF b THEN c1 ELSE c2"
   2.521 +  let ?cs = "ccomp ?if"
   2.522 +  let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"
   2.523 +  
   2.524 +  from `?cs \<turnstile> (0,s,stk) \<rightarrow>^n (size ?cs,t,stk')`
   2.525 +  obtain i' :: int and k m s'' stk'' where
   2.526 +    cs: "?cs \<turnstile> (i',s'',stk'') \<rightarrow>^m (size ?cs,t,stk')" and
   2.527 +        "?bcomp \<turnstile> (0,s,stk) \<rightarrow>^k (i', s'', stk'')" 
   2.528 +        "i' = size ?bcomp \<or> i' = size ?bcomp + size (ccomp c1) + 1"
   2.529 +    by (auto dest!: bcomp_split)
   2.530 +
   2.531 +  hence i':
   2.532 +    "s''=s" "stk'' = stk" 
   2.533 +    "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
   2.534 +    by auto
   2.535 +  
   2.536 +  with cs have cs':
   2.537 +    "ccomp c1@JMP (size (ccomp c2))#ccomp c2 \<turnstile> 
   2.538 +       (if bval b s then 0 else size (ccomp c1)+1, s, stk) \<rightarrow>^m
   2.539 +       (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
   2.540 +    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
   2.541 +     
   2.542 +  show ?case
   2.543 +  proof (cases "bval b s")
   2.544 +    case True with cs'
   2.545 +    show ?thesis
   2.546 +      by simp
   2.547 +         (fastforce dest: exec_n_drop_right 
   2.548 +                   split: split_if_asm simp: exec_n_simps)
   2.549 +  next
   2.550 +    case False with cs'
   2.551 +    show ?thesis
   2.552 +      by (auto dest!: exec_n_drop_Cons exec_n_drop_left 
   2.553 +               simp: exits_Cons isuccs_def)
   2.554 +  qed
   2.555 +next
   2.556 +  case (While b c)
   2.557 +
   2.558 +  from While.prems
   2.559 +  show ?case
   2.560 +  proof (induction n arbitrary: s rule: nat_less_induct)
   2.561 +    case (1 n)
   2.562 +    
   2.563 +    { assume "\<not> bval b s"
   2.564 +      with "1.prems"
   2.565 +      have ?case
   2.566 +        by simp
   2.567 +           (fastforce dest!: bcomp_exec_n bcomp_split 
   2.568 +                     simp: exec_n_simps)
   2.569 +    } moreover {
   2.570 +      assume b: "bval b s"
   2.571 +      let ?c0 = "WHILE b DO c"
   2.572 +      let ?cs = "ccomp ?c0"
   2.573 +      let ?bs = "bcomp b False (size (ccomp c) + 1)"
   2.574 +      let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"
   2.575 +      
   2.576 +      from "1.prems" b
   2.577 +      obtain k where
   2.578 +        cs: "?cs \<turnstile> (size ?bs, s, stk) \<rightarrow>^k (size ?cs, t, stk')" and
   2.579 +        k:  "k \<le> n"
   2.580 +        by (fastforce dest!: bcomp_split)
   2.581 +      
   2.582 +      have ?case
   2.583 +      proof cases
   2.584 +        assume "ccomp c = []"
   2.585 +        with cs k
   2.586 +        obtain m where
   2.587 +          "?cs \<turnstile> (0,s,stk) \<rightarrow>^m (size (ccomp ?c0), t, stk')"
   2.588 +          "m < n"
   2.589 +          by (auto simp: exec_n_step [where k=k])
   2.590 +        with "1.IH"
   2.591 +        show ?case by blast
   2.592 +      next
   2.593 +        assume "ccomp c \<noteq> []"
   2.594 +        with cs
   2.595 +        obtain m m' s'' stk'' where
   2.596 +          c: "ccomp c \<turnstile> (0, s, stk) \<rightarrow>^m' (size (ccomp c), s'', stk'')" and 
   2.597 +          rest: "?cs \<turnstile> (size ?bs + size (ccomp c), s'', stk'') \<rightarrow>^m 
   2.598 +                       (size ?cs, t, stk')" and
   2.599 +          m: "k = m + m'"
   2.600 +          by (auto dest: exec_n_split [where i=0, simplified])
   2.601 +        from c
   2.602 +        have "(c,s) \<Rightarrow> s''" and stk: "stk'' = stk"
   2.603 +          by (auto dest!: While.IH)
   2.604 +        moreover
   2.605 +        from rest m k stk
   2.606 +        obtain k' where
   2.607 +          "?cs \<turnstile> (0, s'', stk) \<rightarrow>^k' (size ?cs, t, stk')"
   2.608 +          "k' < n"
   2.609 +          by (auto simp: exec_n_step [where k=m])
   2.610 +        with "1.IH"
   2.611 +        have "(?c0, s'') \<Rightarrow> t \<and> stk' = stk" by blast
   2.612 +        ultimately
   2.613 +        show ?case using b by blast
   2.614 +      qed
   2.615 +    }
   2.616 +    ultimately show ?case by cases
   2.617 +  qed
   2.618 +qed
   2.619 +
   2.620 +theorem ccomp_exec:
   2.621 +  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk') \<Longrightarrow> (c,s) \<Rightarrow> t"
   2.622 +  by (auto dest: exec_exec_n ccomp_exec_n)
   2.623 +
   2.624 +corollary ccomp_sound:
   2.625 +  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size(ccomp c),t,stk)  \<longleftrightarrow>  (c,s) \<Rightarrow> t"
   2.626 +  by (blast intro!: ccomp_exec ccomp_bigstep)
   2.627 +
   2.628 +end
     3.1 --- a/src/HOL/ROOT	Thu Jun 20 10:15:34 2013 +0200
     3.2 +++ b/src/HOL/ROOT	Thu Jun 20 17:26:16 2013 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4      ASM
     3.5      Finite_Reachable
     3.6      Denotational
     3.7 -    Comp_Rev
     3.8 +    Compiler2
     3.9      Poly_Types
    3.10      Sec_Typing
    3.11      Sec_TypingT