Theory Compiler2

(* Author: Gerwin Klein *)

section ‹Compiler Correctness, Reverse Direction›

theory Compiler2
imports Compiler
begin

text ‹
The preservation of the source code semantics is already shown in the 
parent theory ‹Compiler›. This here shows the second direction.
›

subsection ‹Definitions›

text ‹Execution in \<^term>‹n› steps for simpler induction›
primrec 
  exec_n :: "instr list ⇒ config ⇒ nat ⇒ config ⇒ bool" 
  ("_/ ⊢ (_ →^_/ _)" [65,0,1000,55] 55)
where 
  "P ⊢ c →^0 c' = (c'=c)" |
  "P ⊢ c →^(Suc n) c'' = (∃c'. (P ⊢ c → c') ∧ P ⊢ c' →^n c'')"

text ‹The possible successor PCs of an instruction at position \<^term>‹n››
text_raw‹\snip{isuccsdef}{0}{1}{%›
definition isuccs :: "instr ⇒ int ⇒ int set" where
"isuccs i n = (case i of
  JMP j ⇒ {n + 1 + j} |
  JMPLESS j ⇒ {n + 1 + j, n + 1} |
  JMPGE j ⇒ {n + 1 + j, n + 1} |
  _ ⇒ {n +1})"
text_raw‹}%endsnip›

text ‹The possible successors PCs of an instruction list›
definition succs :: "instr list ⇒ int ⇒ int set" where
"succs P n = {s. ∃i::int. 0 ≤ i ∧ i < size P ∧ s ∈ isuccs (P!!i) (n+i)}" 

text ‹Possible exit PCs of a program›
definition exits :: "instr list ⇒ int set" where
"exits P = succs P 0 - {0..< size P}"

  
subsection ‹Basic properties of \<^term>‹exec_n››

lemma exec_n_exec:
  "P ⊢ c →^n c' ⟹ P ⊢ c →* c'"
  by (induct n arbitrary: c) (auto intro: star.step)

lemma exec_0 [intro!]: "P ⊢ c →^0 c" by simp

lemma exec_Suc:
  "⟦ P ⊢ c → c'; P ⊢ c' →^n c'' ⟧ ⟹ P ⊢ c →^(Suc n) c''" 
  by (fastforce simp del: split_paired_Ex)

lemma exec_exec_n:
  "P ⊢ c →* c' ⟹ ∃n. P ⊢ c →^n c'"
  by (induct rule: star.induct) (auto intro: exec_Suc)
    
lemma exec_eq_exec_n:
  "(P ⊢ c →* c') = (∃n. P ⊢ c →^n c')"
  by (blast intro: exec_exec_n exec_n_exec)

lemma exec_n_Nil [simp]:
  "[] ⊢ c →^k c' = (c' = c ∧ k = 0)"
  by (induct k) (auto simp: exec1_def)

lemma exec1_exec_n [intro!]:
  "P ⊢ c → c' ⟹ P ⊢ c →^1 c'"
  by (cases c') simp


subsection ‹Concrete symbolic execution steps›

lemma exec_n_step:
  "n ≠ n' ⟹ 
  P ⊢ (n,stk,s) →^k (n',stk',s') = 
  (∃c. P ⊢ (n,stk,s) → c ∧ P ⊢ c →^(k - 1) (n',stk',s') ∧ 0 < k)"
  by (cases k) auto

lemma exec1_end:
  "size P <= fst c ⟹ ¬ P ⊢ c → c'"
  by (auto simp: exec1_def)

lemma exec_n_end:
  "size P <= (n::int) ⟹ 
  P ⊢ (n,s,stk) →^k (n',s',stk') = (n' = n ∧ stk'=stk ∧ s'=s ∧ k =0)"
  by (cases k) (auto simp: exec1_end)

lemmas exec_n_simps = exec_n_step exec_n_end


subsection ‹Basic properties of \<^term>‹succs››

lemma succs_simps [simp]: 
  "succs [ADD] n = {n + 1}"
  "succs [LOADI v] n = {n + 1}"
  "succs [LOAD x] n = {n + 1}"
  "succs [STORE x] n = {n + 1}"
  "succs [JMP i] n = {n + 1 + i}"
  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
  by (auto simp: succs_def isuccs_def)

lemma succs_empty [iff]: "succs [] n = {}"
  by (simp add: succs_def)

lemma succs_Cons:
  "succs (x#xs) n = isuccs x n ∪ succs xs (1+n)" (is "_ = ?x ∪ ?xs")
proof 
  let ?isuccs = "λp P n i::int. 0 ≤ i ∧ i < size P ∧ p ∈ isuccs (P!!i) (n+i)"
  have "p ∈ ?x ∪ ?xs" if assm: "p ∈ succs (x#xs) n" for p
  proof -
    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i"
      unfolding succs_def by auto     
    show ?thesis
    proof cases
      assume "i = 0" with isuccs show ?thesis by simp
    next
      assume "i ≠ 0" 
      with isuccs 
      have "?isuccs p xs (1+n) (i - 1)" by auto
      hence "p ∈ ?xs" unfolding succs_def by blast
      thus ?thesis .. 
    qed
  qed
  thus "succs (x#xs) n ⊆ ?x ∪ ?xs" ..

  have "p ∈ succs (x#xs) n" if assm: "p ∈ ?x ∨ p ∈ ?xs" for p
  proof -
    from assm show ?thesis
    proof
      assume "p ∈ ?x" thus ?thesis by (fastforce simp: succs_def)
    next
      assume "p ∈ ?xs"
      then obtain i where "?isuccs p xs (1+n) i"
        unfolding succs_def by auto
      hence "?isuccs p (x#xs) n (1+i)"
        by (simp add: algebra_simps)
      thus ?thesis unfolding succs_def by blast
    qed
  qed
  thus "?x ∪ ?xs ⊆ succs (x#xs) n" by blast
qed

lemma succs_iexec1:
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 ≤ i" "i < size P"
  shows "fst c' ∈ succs P 0"
  using assms by (auto simp: succs_def isuccs_def split: instr.split)

lemma succs_shift:
  "(p - n ∈ succs P 0) = (p ∈ succs P n)" 
  by (fastforce simp: succs_def isuccs_def split: instr.split)
  
lemma inj_op_plus [simp]:
  "inj ((+) (i::int))"
  by (metis add_minus_cancel inj_on_inverseI)

lemma succs_set_shift [simp]:
  "(+) i ` succs xs 0 = succs xs i"
  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)

lemma succs_append [simp]:
  "succs (xs @ ys) n = succs xs n ∪ succs ys (n + size xs)"
  by (induct xs arbitrary: n) (auto simp: succs_Cons algebra_simps)


lemma exits_append [simp]:
  "exits (xs @ ys) = exits xs ∪ ((+) (size xs)) ` exits ys - 
                     {0..<size xs + size ys}" 
  by (auto simp: exits_def image_set_diff)
  
lemma exits_single:
  "exits [x] = isuccs x 0 - {0}"
  by (auto simp: exits_def succs_def)
  
lemma exits_Cons:
  "exits (x # xs) = (isuccs x 0 - {0}) ∪ ((+) 1) ` exits xs - 
                     {0..<1 + size xs}" 
  using exits_append [of "[x]" xs]
  by (simp add: exits_single)

lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)

lemma exits_simps [simp]:
  "exits [ADD] = {1}"
  "exits [LOADI v] = {1}"
  "exits [LOAD x] = {1}"
  "exits [STORE x] = {1}"
  "i ≠ -1 ⟹ exits [JMP i] = {1 + i}"
  "i ≠ -1 ⟹ exits [JMPGE i] = {1 + i, 1}"
  "i ≠ -1 ⟹ exits [JMPLESS i] = {1 + i, 1}"
  by (auto simp: exits_def)

lemma acomp_succs [simp]:
  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
  by (induct a arbitrary: n) auto

lemma acomp_size:
  "(1::int) ≤ size (acomp a)"
  by (induct a) auto

lemma acomp_exits [simp]:
  "exits (acomp a) = {size (acomp a)}"
  by (auto simp: exits_def acomp_size)

lemma bcomp_succs:
  "0 ≤ i ⟹
  succs (bcomp b f i) n ⊆ {n .. n + size (bcomp b f i)}
                           ∪ {n + i + size (bcomp b f i)}" 
proof (induction b arbitrary: f i n)
  case (And b1 b2)
  from And.prems
  show ?case 
    by (cases f)
       (auto dest: And.IH(1) [THEN subsetD, rotated] 
                   And.IH(2) [THEN subsetD, rotated])
qed auto

lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]

lemma bcomp_exits:
  fixes i :: int
  shows
  "0 ≤ i ⟹
  exits (bcomp b f i) ⊆ {size (bcomp b f i), i + size (bcomp b f i)}" 
  by (auto simp: exits_def)
  
lemma bcomp_exitsD [dest!]:
  "p ∈ exits (bcomp b f i) ⟹ 0 ≤ i ⟹ 
  p = size (bcomp b f i) ∨ p = i + size (bcomp b f i)"
  using bcomp_exits by auto

lemma ccomp_succs:
  "succs (ccomp c) n ⊆ {n..n + size (ccomp c)}"
proof (induction c arbitrary: n)
  case SKIP thus ?case by simp
next
  case Assign thus ?case by simp
next
  case (Seq c1 c2)
  from Seq.prems
  show ?case 
    by (fastforce dest: Seq.IH [THEN subsetD])
next
  case (If b c1 c2)
  from If.prems
  show ?case
    by (auto dest!: If.IH [THEN subsetD] simp: isuccs_def succs_Cons)
next
  case (While b c)
  from While.prems
  show ?case by (auto dest!: While.IH [THEN subsetD])
qed

lemma ccomp_exits:
  "exits (ccomp c) ⊆ {size (ccomp c)}"
  using ccomp_succs [of c 0] by (auto simp: exits_def)

lemma ccomp_exitsD [dest!]:
  "p ∈ exits (ccomp c) ⟹ p = size (ccomp c)"
  using ccomp_exits by auto


subsection ‹Splitting up machine executions›

lemma exec1_split:
  fixes i j :: int
  shows
  "P @ c @ P' ⊢ (size P + i, s) → (j,s') ⟹ 0 ≤ i ⟹ i < size c ⟹ 
  c ⊢ (i,s) → (j - size P, s')"
  by (auto split: instr.splits simp: exec1_def)

lemma exec_n_split:
  fixes i j :: int
  assumes "P @ c @ P' ⊢ (size P + i, s) →^n (j, s')"
          "0 ≤ i" "i < size c" 
          "j ∉ {size P ..< size P + size c}"
  shows "∃s'' (i'::int) k m. 
                   c ⊢ (i, s) →^k (i', s'') ∧
                   i' ∈ exits c ∧ 
                   P @ c @ P' ⊢ (size P + i', s'') →^m (j, s') ∧
                   n = k + m" 
using assms proof (induction n arbitrary: i j s)
  case 0
  thus ?case by simp
next
  case (Suc n)
  have i: "0 ≤ i" "i < size c" by fact+
  from Suc.prems
  have j: "¬ (size P ≤ j ∧ j < size P + size c)" by simp
  from Suc.prems 
  obtain i0 s0 where
    step: "P @ c @ P' ⊢ (size P + i, s) → (i0,s0)" and
    rest: "P @ c @ P' ⊢ (i0,s0) →^n (j, s')"
    by clarsimp

  from step i
  have c: "c ⊢ (i,s) → (i0 - size P, s0)" by (rule exec1_split)

  have "i0 = size P + (i0 - size P) " by simp
  then obtain j0::int where j0: "i0 = size P + j0"  ..

  note split_paired_Ex [simp del]

  have ?case if assm: "j0 ∈ {0 ..< size c}"
  proof -
    from assm j0 j rest c show ?case
      by (fastforce dest!: Suc.IH intro!: exec_Suc)
  qed
  moreover
  have ?case if assm: "j0 ∉ {0 ..< size c}"
  proof -
    from c j0 have "j0 ∈ succs c 0"
      by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
    with assm have "j0 ∈ exits c" by (simp add: exits_def)
    with c j0 rest show ?case by fastforce
  qed
  ultimately
  show ?case by cases
qed

lemma exec_n_drop_right:
  fixes j :: int
  assumes "c @ P' ⊢ (0, s) →^n (j, s')" "j ∉ {0..<size c}"
  shows "∃s'' i' k m. 
          (if c = [] then s'' = s ∧ i' = 0 ∧ k = 0
           else c ⊢ (0, s) →^k (i', s'') ∧
           i' ∈ exits c) ∧ 
           c @ P' ⊢ (i', s'') →^m (j, s') ∧
           n = k + m"
  using assms
  by (cases "c = []")
     (auto dest: exec_n_split [where P="[]", simplified])
  

text ‹
  Dropping the left context of a potentially incomplete execution of \<^term>‹c›.
›

lemma exec1_drop_left:
  fixes i n :: int
  assumes "P1 @ P2 ⊢ (i, s, stk) → (n, s', stk')" and "size P1 ≤ i"
  shows "P2 ⊢ (i - size P1, s, stk) → (n - size P1, s', stk')"
proof -
  have "i = size P1 + (i - size P1)" by simp 
  then obtain i' :: int where "i = size P1 + i'" ..
  moreover
  have "n = size P1 + (n - size P1)" by simp 
  then obtain n' :: int where "n = size P1 + n'" ..
  ultimately 
  show ?thesis using assms 
    by (clarsimp simp: exec1_def simp del: iexec.simps)
qed

lemma exec_n_drop_left:
  fixes i n :: int
  assumes "P @ P' ⊢ (i, s, stk) →^k (n, s', stk')"
          "size P ≤ i" "exits P' ⊆ {0..}"
  shows "P' ⊢ (i - size P, s, stk) →^k (n - size P, s', stk')"
using assms proof (induction k arbitrary: i s stk)
  case 0 thus ?case by simp
next
  case (Suc k)
  from Suc.prems
  obtain i' s'' stk'' where
    step: "P @ P' ⊢ (i, s, stk) → (i', s'', stk'')" and
    rest: "P @ P' ⊢ (i', s'', stk'') →^k (n, s', stk')"
    by auto
  from step ‹size P ≤ i›
  have *: "P' ⊢ (i - size P, s, stk) → (i' - size P, s'', stk'')" 
    by (rule exec1_drop_left)
  then have "i' - size P ∈ succs P' 0"
    by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
  with ‹exits P' ⊆ {0..}›
  have "size P ≤ i'" by (auto simp: exits_def)
  from rest this ‹exits P' ⊆ {0..}›     
  have "P' ⊢ (i' - size P, s'', stk'') →^k (n - size P, s', stk')"
    by (rule Suc.IH)
  with * show ?case by auto
qed

lemmas exec_n_drop_Cons = 
  exec_n_drop_left [where P="[instr]", simplified] for instr

definition
  "closed P ⟷ exits P ⊆ {size P}" 

lemma ccomp_closed [simp, intro!]: "closed (ccomp c)"
  using ccomp_exits by (auto simp: closed_def)

lemma acomp_closed [simp, intro!]: "closed (acomp c)"
  by (simp add: closed_def)

lemma exec_n_split_full:
  fixes j :: int
  assumes exec: "P @ P' ⊢ (0,s,stk) →^k (j, s', stk')"
  assumes P: "size P ≤ j" 
  assumes closed: "closed P"
  assumes exits: "exits P' ⊆ {0..}"
  shows "∃k1 k2 s'' stk''. P ⊢ (0,s,stk) →^k1 (size P, s'', stk'') ∧ 
                           P' ⊢ (0,s'',stk'') →^k2 (j - size P, s', stk')"
proof (cases "P")
  case Nil with exec
  show ?thesis by fastforce
next
  case Cons
  hence "0 < size P" by simp
  with exec P closed
  obtain k1 k2 s'' stk'' where
    1: "P ⊢ (0,s,stk) →^k1 (size P, s'', stk'')" and
    2: "P @ P' ⊢ (size P,s'',stk'') →^k2 (j, s', stk')"
    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified] 
             simp: closed_def)
  moreover
  have "j = size P + (j - size P)" by simp
  then obtain j0 :: int where "j = size P + j0" ..
  ultimately
  show ?thesis using exits
    by (fastforce dest: exec_n_drop_left)
qed


subsection ‹Correctness theorem›

lemma acomp_neq_Nil [simp]:
  "acomp a ≠ []"
  by (induct a) auto

lemma acomp_exec_n [dest!]:
  "acomp a ⊢ (0,s,stk) →^n (size (acomp a),s',stk') ⟹ 
  s' = s ∧ stk' = aval a s#stk"
proof (induction a arbitrary: n s' stk stk')
  case (Plus a1 a2)
  let ?sz = "size (acomp a1) + (size (acomp a2) + 1)"
  from Plus.prems
  have "acomp a1 @ acomp a2 @ [ADD] ⊢ (0,s,stk) →^n (?sz, s', stk')" 
    by (simp add: algebra_simps)
      
  then obtain n1 s1 stk1 n2 s2 stk2 n3 where 
    "acomp a1 ⊢ (0,s,stk) →^n1 (size (acomp a1), s1, stk1)"
    "acomp a2 ⊢ (0,s1,stk1) →^n2 (size (acomp a2), s2, stk2)" 
       "[ADD] ⊢ (0,s2,stk2) →^n3 (1, s', stk')"
    by (auto dest!: exec_n_split_full)

  thus ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
qed (auto simp: exec_n_simps exec1_def)

lemma bcomp_split:
  fixes i j :: int
  assumes "bcomp b f i @ P' ⊢ (0, s, stk) →^n (j, s', stk')" 
          "j ∉ {0..<size (bcomp b f i)}" "0 ≤ i"
  shows "∃s'' stk'' (i'::int) k m. 
           bcomp b f i ⊢ (0, s, stk) →^k (i', s'', stk'') ∧
           (i' = size (bcomp b f i) ∨ i' = i + size (bcomp b f i)) ∧
           bcomp b f i @ P' ⊢ (i', s'', stk'') →^m (j, s', stk') ∧
           n = k + m"
  using assms by (cases "bcomp b f i = []") (fastforce dest!: exec_n_drop_right)+

lemma bcomp_exec_n [dest]:
  fixes i j :: int
  assumes "bcomp b f j ⊢ (0, s, stk) →^n (i, s', stk')"
          "size (bcomp b f j) ≤ i" "0 ≤ j"
  shows "i = size(bcomp b f j) + (if f = bval b s then j else 0) ∧
         s' = s ∧ stk' = stk"
using assms proof (induction b arbitrary: f j i n s' stk')
  case Bc thus ?case 
    by (simp split: if_split_asm add: exec_n_simps exec1_def)
next
  case (Not b) 
  from Not.prems show ?case
    by (fastforce dest!: Not.IH) 
next
  case (And b1 b2)
  
  let ?b2 = "bcomp b2 f j" 
  let ?m  = "if f then size ?b2 else size ?b2 + j"
  let ?b1 = "bcomp b1 False ?m" 

  have j: "size (bcomp (And b1 b2) f j) ≤ i" "0 ≤ j" by fact+
  
  from And.prems
  obtain s'' stk'' and i'::int and k m where 
    b1: "?b1 ⊢ (0, s, stk) →^k (i', s'', stk'')"
        "i' = size ?b1 ∨ i' = ?m + size ?b1" and
    b2: "?b2 ⊢ (i' - size ?b1, s'', stk'') →^m (i - size ?b1, s', stk')"
    by (auto dest!: bcomp_split dest: exec_n_drop_left)
  from b1 j
  have "i' = size ?b1 + (if ¬bval b1 s then ?m else 0) ∧ s'' = s ∧ stk'' = stk"
    by (auto dest!: And.IH)
  with b2 j
  show ?case 
    by (fastforce dest!: And.IH simp: exec_n_end split: if_split_asm)
next
  case Less
  thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *) 
qed

lemma ccomp_empty [elim!]:
  "ccomp c = [] ⟹ (c,s) ⇒ s"
  by (induct c) auto

declare assign_simp [simp]

lemma ccomp_exec_n:
  "ccomp c ⊢ (0,s,stk) →^n (size(ccomp c),t,stk')
  ⟹ (c,s) ⇒ t ∧ stk'=stk"
proof (induction c arbitrary: s t stk stk' n)
  case SKIP
  thus ?case by auto
next
  case (Assign x a)
  thus ?case
    by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps exec1_def)
next
  case (Seq c1 c2)
  thus ?case by (fastforce dest!: exec_n_split_full)
next
  case (If b c1 c2)
  note If.IH [dest!]

  let ?if = "IF b THEN c1 ELSE c2"
  let ?cs = "ccomp ?if"
  let ?bcomp = "bcomp b False (size (ccomp c1) + 1)"
  
  from ‹?cs ⊢ (0,s,stk) →^n (size ?cs,t,stk')›
  obtain i' :: int and k m s'' stk'' where
    cs: "?cs ⊢ (i',s'',stk'') →^m (size ?cs,t,stk')" and
        "?bcomp ⊢ (0,s,stk) →^k (i', s'', stk'')" 
        "i' = size ?bcomp ∨ i' = size ?bcomp + size (ccomp c1) + 1"
    by (auto dest!: bcomp_split)

  hence i':
    "s''=s" "stk'' = stk" 
    "i' = (if bval b s then size ?bcomp else size ?bcomp+size(ccomp c1)+1)"
    by auto
  
  with cs have cs':
    "ccomp c1@JMP (size (ccomp c2))#ccomp c2 ⊢ 
       (if bval b s then 0 else size (ccomp c1)+1, s, stk) →^m
       (1 + size (ccomp c1) + size (ccomp c2), t, stk')"
    by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
     
  show ?case
  proof (cases "bval b s")
    case True with cs'
    show ?thesis
      by simp
         (fastforce dest: exec_n_drop_right 
                   split: if_split_asm
                   simp: exec_n_simps exec1_def)
  next
    case False with cs'
    show ?thesis
      by (auto dest!: exec_n_drop_Cons exec_n_drop_left 
               simp: exits_Cons isuccs_def)
  qed
next
  case (While b c)

  from While.prems
  show ?case
  proof (induction n arbitrary: s rule: nat_less_induct)
    case (1 n)

    have ?case if assm: "¬ bval b s"
    proof -
      from assm "1.prems"
      show ?case
        by simp (fastforce dest!: bcomp_split simp: exec_n_simps)
    qed
    moreover
    have ?case if b: "bval b s"
    proof -
      let ?c0 = "WHILE b DO c"
      let ?cs = "ccomp ?c0"
      let ?bs = "bcomp b False (size (ccomp c) + 1)"
      let ?jmp = "[JMP (-((size ?bs + size (ccomp c) + 1)))]"
      
      from "1.prems" b
      obtain k where
        cs: "?cs ⊢ (size ?bs, s, stk) →^k (size ?cs, t, stk')" and
        k:  "k ≤ n"
        by (fastforce dest!: bcomp_split)
      
      show ?case
      proof cases
        assume "ccomp c = []"
        with cs k
        obtain m where
          "?cs ⊢ (0,s,stk) →^m (size (ccomp ?c0), t, stk')"
          "m < n"
          by (auto simp: exec_n_step [where k=k] exec1_def)
        with "1.IH"
        show ?case by blast
      next
        assume "ccomp c ≠ []"
        with cs
        obtain m m' s'' stk'' where
          c: "ccomp c ⊢ (0, s, stk) →^m' (size (ccomp c), s'', stk'')" and 
          rest: "?cs ⊢ (size ?bs + size (ccomp c), s'', stk'') →^m 
                       (size ?cs, t, stk')" and
          m: "k = m + m'"
          by (auto dest: exec_n_split [where i=0, simplified])
        from c
        have "(c,s) ⇒ s''" and stk: "stk'' = stk"
          by (auto dest!: While.IH)
        moreover
        from rest m k stk
        obtain k' where
          "?cs ⊢ (0, s'', stk) →^k' (size ?cs, t, stk')"
          "k' < n"
          by (auto simp: exec_n_step [where k=m] exec1_def)
        with "1.IH"
        have "(?c0, s'') ⇒ t ∧ stk' = stk" by blast
        ultimately
        show ?case using b by blast
      qed
    qed
    ultimately show ?case by cases
  qed
qed

theorem ccomp_exec:
  "ccomp c ⊢ (0,s,stk) →* (size(ccomp c),t,stk') ⟹ (c,s) ⇒ t"
  by (auto dest: exec_exec_n ccomp_exec_n)

corollary ccomp_sound:
  "ccomp c ⊢ (0,s,stk) →* (size(ccomp c),t,stk)  ⟷  (c,s) ⇒ t"
  by (blast intro!: ccomp_exec ccomp_bigstep)

end