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