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