Theory Compiler2

(*  Title:       A Reuse-Based Multi-Stage Compiler Verification for Language IMP
    Author:      Pasquale Noce
                 Senior Staff Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Compiler verification"

theory Compiler2
  imports Compiler
begin

text ‹
The reasoning toolbox introduced in the @{text Compiler2} theory of cite‹"Noce21"› to cope with
the ``hard'' direction of the bisimulation proof can be outlined as follows.

First, predicate @{text execl_all} is defined to capture the notion of a \emph{complete small-step}
program execution -- an \emph{assembly} program execution in the current context --, where such an
execution is modeled as a list of program configurations. This predicate has the property that, for
any complete execution of program @{term "P @ P' @ P''"} making the program counter point to the
beginning of program @{term P'} in some step, there exists a sub-execution being also a complete
execution of @{term P'}. Under the further assumption that any complete execution of @{term P'}
fulfills a given predicate @{term Q}, this implies the existence of a sub-execution fulfilling
@{term Q} (as established by lemma @{text execl_all_sub} in cite‹"Noce21"›).

The compilation of arithmetic/boolean expressions and commands, modeled by functions @{const acomp},
@{const bcomp}, and @{const ccomp}, produces programs matching pattern @{term "P @ P' @ P''"}, where
sub-programs @{term P}, @{term P'}, @{term P''} may either be empty or result from the compilation
of nested expressions or commands (possibly with the insertion of further instructions). Moreover,
simulation of compiled programs by source ones can be formalized as the statement that any complete
small-step execution of a compiled program meets a proper well-behavedness predicate @{text cpred}.
By proving this statement via structural induction over commands, the resulting subgoals assume its
validity for any nested command. If as many suitable well-behavedness predicates, @{text apred} and
@{text bpred}, have been proven to hold for any complete execution of a compiled arithmetic/boolean
expression, the above @{text execl_all}'s property entails that the complete execution targeted in
each subgoal is comprised of pieces satisfying @{text apred}, @{text bpred}, or @{text cpred}, which
enables to conclude that the whole execution satisfies @{text cpred}.

Can this machinery come in handy to generalize single-step assembly code simulation by machine code,
established by lemma @{thm [source] exec1_m_exec1}, to full program executions? Actually, the gap
to be filled in is showing that assembly program execution unfolds in such a way, that a machine
stack pointer starting from zero complies with @{thm [source] exec1_m_exec1}'s assumptions in each
intermediate step. The key insight, which provides the previous question with an affirmative answer,
is that this property can as well be formalized as a well-behavedness predicate @{text mpred}, so
that the pending task takes again the form of proving that such a predicate holds for any complete
small-step execution of an assembly program.

Following this insight, the present theory extends the @{text Compiler2} theory of cite‹"Noce21"›
by reusing its reasoning toolbox to additionally prove that any such program execution is indeed
well-behaved in this respect, too.
›


subsection "Preliminary definitions and lemmas"

text ‹
To define predicate @{text mpred}, the value taken by the machine stack pointer in every program
execution step needs to be expressed as a function of just the initial configuration and the current
one, so that a quantification over each intermediate configuration can occur in the definition's
right-hand side. On the other hand, within @{thm [source] exec1_m_exec1}'s conclusion, the stack
pointer @{term sp'} resulting from single-step execution is @{term "sp + length stk' - length stk"},
where @{term stk} and @{term sp} are the assembly stack and the stack pointer prior to single-step
execution and @{term stk'} is the ensuing assembly stack. Thus, the aforesaid function must be such
that, by replacing @{term sp} with its value into the previous expression, @{term sp'}'s value is
obtained. If @{prop "sp = length stk - length stk0"}, where @{term stk0} is the initial assembly
stack, that expression gives @{prop "sp' = length stk - length stk0 + length stk' - length stk"},
and the right-hand side matches @{term "length stk' - length stk0"} by library lemma @{thm [source]
add_diff_assoc2} provided that @{prop "length stk0 ≤ length stk"}.

Thus, to meet @{thm [source] exec1_m_exec1}'s former assumption for an assembly program @{term P},
each intermediate configuration @{term "(pc, s, stk)"} in a list @{term cfs} must be such that (i)
@{term "length stk - length stk0"} is not less than the number of the operands taken by @{term P}'s
instruction at offset @{term pc}, and (ii) @{prop "length stk0 ≤ length stk"}. Since the subgoals
arising from structural induction will assume this to hold for pieces of a given complete execution,
it is convenient to make @{text mpred} take two offsets @{term m} and @{term n} as further inputs
besides @{term P} and @{term cfs}. This enables the quantification to only span the configurations
within @{term cfs} whose offsets are comprised in the interval @{term "{m..<n}"} (the upper bound is
excluded as intermediate configurations alone are relevant). Unlike @{text apred}, @{text bpred},
and @{text cpred}, @{text mpred} expresses a well-behavedness condition applying indiscriminately to
arithmetic/boolean expressions and commands, which is the reason why a single predicate suffices, as
long as it takes a list of assembly instructions as input instead of a specific source code token.

\null
›

fun execl :: "instr list ⇒ config list ⇒ bool" (infix ‹⊨› 55) where
"P ⊨ cf # cf' # cfs = (P ⊢ cf → cf' ∧ P ⊨ cf' # cfs)" |
"P ⊨ _ = True"

definition execl_all :: "instr list ⇒ config list ⇒ bool" (‹(_/ ⊨/ _□)› 55) where
"P ⊨ cfs□ ≡ P ⊨ cfs ∧ cfs ≠ [] ∧
  fst (cfs ! 0) = 0 ∧ fst (cfs ! (length cfs - 1)) ∉ {0..<size P}"

definition apred :: "aexp ⇒ config ⇒ config ⇒ bool" where
"apred ≡ λa (pc, s, stk) (pc', s', stk').
  pc' = pc + size (acomp a) ∧ s' = s ∧ stk' = aval a s # stk"

definition bpred :: "bexp × bool × int ⇒ config ⇒ config ⇒ bool" where
"bpred ≡ λ(b, f, i) (pc, s, stk) (pc', s', stk').
  pc' = pc + size (bcomp (b, f, i)) + (if bval b s = f then i else 0) ∧
    s' = s ∧ stk' = stk"

definition cpred :: "com ⇒ config ⇒ config ⇒ bool" where
"cpred ≡ λc (pc, s, stk) (pc', s', stk').
  pc' = pc + size (ccomp c) ∧ (c, s) ⇒ s' ∧ stk' = stk"

definition mpred :: "instr list ⇒ config list ⇒ nat ⇒ nat ⇒ bool" where
"mpred P cfs m n ≡ case cfs ! 0 of (_, _, stk0) ⇒
  ∀k ∈ {m..<n}. case cfs ! k of (pc, _, stk) ⇒
    msp P pc ≤ length stk - length stk0 ∧ length stk0 ≤ length stk"

abbreviation off :: "instr list ⇒ config ⇒ config" where
"off P cf ≡ (fst cf - size P, snd cf)"

text ‹
\null

By slightly extending their conclusions, the lemmas used to prove compiler correctness automatically
for constructors @{const N}, @{const V}, @{const Bc}, and @{const SKIP} can be reused for the new
well-behavedness proof as well. Actually, it is sufficient to additionally infer that (i) the given
complete execution consists of one or two steps and (ii) in the latter case, the initial program
counter is zero, so that the first inequality within @{const mpred}'s definition matches the trivial
one $0 \leq 0$.

\null
›

lemma iexec_offset [intro]:
 "(ins, pc, s, stk) ↦ (pc', s', stk') ⟹
    (ins, pc - i, s, stk) ↦ (pc' - i, s', stk')"
by (auto simp: iexec_simp split: instr.split)

lemma execl_next:
 "⟦P ⊨ cfs; k < length cfs; k ≠ length cfs - 1⟧ ⟹
    (P !! fst (cfs ! k), cfs ! k) ↦ cfs ! Suc k ∧
      0 ≤ fst (cfs ! k) ∧ fst (cfs ! k) < size P"
by (induction cfs arbitrary: k rule: execl.induct, auto
 simp: nth_Cons exec1_def split: nat.split)

lemma execl_last:
 "⟦P ⊨ cfs; k < length cfs; fst (cfs ! k) ∉ {0..<size P}⟧ ⟹
    length cfs - 1 = k"
by (induction cfs arbitrary: k rule: execl.induct, auto
 simp: nth_Cons exec1_def split: nat.split_asm)

lemma execl_take:
 "P ⊨ cfs ⟹ P ⊨ take n cfs"
by (induction cfs arbitrary: n rule: execl.induct, simp_all (no_asm_simp)
 add: take_Cons split: nat.split, subst take_Suc_Cons [symmetric], fastforce)

lemma execl_drop:
 "P ⊨ cfs ⟹ P ⊨ drop n cfs"
by (induction cfs arbitrary: n rule: execl.induct, simp_all
 add: drop_Cons split: nat.split)

lemma execl_all_N [simplified, dest]:
 "[LOADI i] ⊨ cfs□ ⟹ apred (N i) (cfs ! 0) (cfs ! (length cfs - 1)) ∧
    length cfs = 2 ∧ fst (cfs ! 0) = 0"
by (clarsimp simp: execl_all_def apred_def, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [!] execl_next,
 ((rule ccontr)?, fastforce, (rule execl_last)?)+)

lemma execl_all_V [simplified, dest]:
 "[LOAD x] ⊨ cfs□ ⟹ apred (V x) (cfs ! 0) (cfs ! (length cfs - 1)) ∧
    length cfs = 2 ∧ fst (cfs ! 0) = 0"
by (clarsimp simp: execl_all_def apred_def, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [!] execl_next,
 ((rule ccontr)?, fastforce, (rule execl_last)?)+)

lemma execl_all_Bc [simplified, dest]:
 "⟦if v = f then [JMP i] else [] ⊨ cfs□; 0 ≤ i⟧ ⟹
    bpred (Bc v, f, i) (cfs ! 0) (cfs ! (length cfs - 1)) ∧
    length cfs = (if v = f then 2 else 1) ∧ fst (cfs ! 0) = 0"
by (clarsimp simp: execl_all_def bpred_def split: if_split_asm, cases "cfs ! 0",
 subgoal_tac "length cfs - 1 = 1", frule_tac [1-2] execl_next,
 ((rule ccontr)?, force, (rule execl_last)?)+, rule execl.cases [of "([], cfs)"],
 auto simp: exec1_def)

lemma execl_all_SKIP [simplified, dest]:
 "[] ⊨ cfs□ ⟹ cpred SKIP (cfs ! 0) (cfs ! (length cfs - 1)) ∧ length cfs = 1"
by (rule execl.cases [of "([], cfs)"], auto simp: execl_all_def exec1_def cpred_def)

text ‹
\null

In cite‹"Noce21"›, part of the proof of lemma @{text execl_all_sub} is devoted to establishing the
fundamental property of predicate @{const execl_all} stated above: for any complete execution of
program @{term "P @ P' @ P''"} making the program counter point to the beginning of @{term P'} in
its @{term k}-th step, there exists a sub-execution starting from the @{term k}-th step and being a
complete execution of @{term P'}.

Here below, this property is proven as a lemma in its own respect, named @{text execl_all}, so that
besides @{text execl_all_sub}, it can be reused to prove a further lemma @{text execl_all_sub_m}.
This new lemma establishes that, if (i) @{text execl_all_sub}'s assumptions hold, (ii) any complete
execution of @{term P'} fulfills predicate @{const mpred}, and (iii) the initial assembly stack is
not longer than the one in the @{term k}-th step, then there exists a sub-execution starting from
the @{term k}-th step and fulfilling both predicates @{term Q} and @{const mpred}. Within the new
well-behavedness proof, this lemma will play the same role as @{text execl_all_sub} in the compiler
correctness proof; namely, for each structural induction subgoal, it will entail that the respective
complete execution is comprised of pieces fulfilling @{const mpred}. As with @{text execl_all_sub},
@{term Q} can be instantiated to @{const apred}, @{const bpred}, or @{const cpred}; indeed, knowing
that sub-executions satisfy these predicates in addition to @{const mpred} is necessary to show that
the whole execution satisfies @{const mpred}. For example, to draw the conclusion that the assembly
code @{term "acomp a @ [STORE x]"} for an assignment meets @{const mpred}, one needs to know that
@{term "acomp a"}'s sub-execution also meets @{const apred}, so that the assembly stack contains an
element more than the initial stack when instruction @{term "STORE x"} is executed.

\null
›

lemma execl_sub_aux:
 "⟦⋀m n. ∀k ∈ {m..<n}. Q P' (((pc, s, stk) # cfs) ! k) ⟹ P' ⊨
    map (off P) (case m of 0 ⇒ (pc, s, stk) # take n cfs | Suc m ⇒ F cfs m n);
    ∀k ∈ {m..<n+m+length cfs'}. Q P' ((cfs' @ (pc, s, stk) # cfs) ! (k-m))⟧ ⟹
  P' ⊨ (pc - size P, s, stk) # map (off P) (take n cfs)"
  (is "⟦⋀_ _. ∀k ∈ _. Q P' (?F k) ⟹ _; ∀k ∈ ?A. Q P' (?G k)⟧ ⟹ _")
by (subgoal_tac "∀k ∈ {0..<n}. Q P' (?F k)", fastforce, subgoal_tac
 "∀k ∈ {0..<n}. k + m + length cfs' ∈ ?A ∧ ?F k = ?G (k + m + length cfs')",
 fastforce, simp add: nth_append)

lemma execl_sub:
 "⟦P @ P' @ P'' ⊨ cfs; ∀k ∈ {m..<n}.
     size P ≤ fst (cfs ! k) ∧ fst (cfs ! k) - size P < size P'⟧ ⟹
   P' ⊨ map (off P) (drop m (take (Suc n) cfs))"
  (is "⟦_; ∀k ∈ _. ?P P' cfs k⟧ ⟹ P' ⊨ map _ (?F cfs m (Suc n))")
proof (induction cfs arbitrary: m n rule: execl.induct [of _ P'], auto
 simp: take_Cons drop_Cons exec1_def split: nat.split, force, force, force,
 erule execl_sub_aux [where m = 0], subst append_Cons [of _ "[]"], simp,
 erule execl_sub_aux [where m = "Suc 0" and cfs' = "[]"], simp)
  fix P' pc s stk cfs m n
  let ?cf = "(pc, s, stk) :: config"
  assume "⋀m n. ∀k ∈ {m..<n}. ?P P' (?cf # cfs) k ⟹ P' ⊨
    map (off P) (case m of 0 ⇒ ?cf # take n cfs | Suc m ⇒ ?F cfs m n)"
  moreover assume "∀k ∈ {Suc (Suc m)..<Suc n}. ?P P' cfs (k - Suc (Suc 0))"
  hence "∀k ∈ {Suc m..<n}. ?P P' (?cf # cfs) k"
    by force
  ultimately show "P' ⊨ map (off P) (?F cfs m n)"
    by fastforce
qed

lemma execl_all:
  assumes
    A: "P @ P' x @ P'' ⊨ cfs□" and
    B: "k < length cfs" and
    C: "fst (cfs ! k) = size P"
  shows "∃k' ∈ {k..<length cfs}. P' x ⊨ map (off P) (drop k (take (Suc k') cfs))□"
    (is "∃k' ∈ _. _ ⊨ ?F k'□")
proof -
  let ?P = "λk. size P ≤ fst (cfs ! k) ∧ fst (cfs ! k) - size P < size (P' x)"
  let ?A = "{k'. k' ∈ {k..<length cfs} ∧ ¬ ?P k'}"
  have D: "Min ?A ∈ ?A"
    (is "?k' ∈ _")
    using A and B by (rule_tac Min_in, simp_all add: execl_all_def,
     rule_tac exI [of _ "length cfs - 1"], auto)
  moreover from this have "?F ?k' ! (length (?F ?k') - 1) = off P (cfs ! ?k')"
    by (auto dest!: min_absorb2 simp: less_eq_Suc_le)
  moreover have "¬ (∃k'. k' ∈ {k'. k' ∈ {k..<?k'} ∧ ¬ ?P k'})"
    by (rule notI, erule exE, frule rev_subsetD [of _ _ ?A], rule subsetI,
     insert D, simp, subgoal_tac "finite ?A", drule Min_le, force+)
  hence "P' x ⊨ ?F ?k'"
    using A by (subst (asm) execl_all_def, rule_tac execl_sub, blast+)
  ultimately show ?thesis
    using C by (auto simp: execl_all_def)
qed

lemma execl_all_sub [rule_format]:
  assumes
    A: "P @ P' x @ P'' ⊨ cfs□" and
    B: "k < length cfs" and
    C: "fst (cfs ! k) = size P" and
    D: "∀cfs. P' x ⊨ cfs□ ⟶ Q x (cfs ! 0) (cfs ! (length cfs - 1))"
  shows "∃k' < length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k'))"
proof -
  have "∃k' ∈ {k..<length cfs}. P' x ⊨ map (off P) (drop k (take (Suc k') cfs))□"
    (is "∃k' ∈ _. _ ⊨ ?F k'□")
    using A and B and C by (rule execl_all)
  then obtain k' where "k' ∈ {k..<length cfs}" and
   "Q x (?F k' ! 0) (?F k' ! (length (?F k') - 1))"
    using D by blast
  moreover from this have "?F k' ! (length (?F k') - 1) = off P (cfs ! k')"
    by (auto dest!: min_absorb2 simp: less_eq_Suc_le)
  ultimately show ?thesis
    by auto
qed

lemma execl_all_sub2:
  assumes
    A: "P x @ P' x' @ P'' ⊨ cfs□"
      (is "?P ⊨ _□") and
    B: "⋀cfs. P x ⊨ cfs□ ⟹ (λ(pc, s, stk) (pc', s', stk').
      pc' = pc + size (P x) + I s ∧ Q s s' ∧ stk' = F s stk)
        (cfs ! 0) (cfs ! (length cfs - 1))"
      (is "⋀cfs. _ ⟹ ?Q x (cfs ! 0) (cfs ! (length cfs - 1))") and
    C: "⋀cfs. P' x' ⊨ cfs□ ⟹ (λ(pc, s, stk) (pc', s', stk').
      pc' = pc + size (P' x') + I' s ∧ Q' s s' ∧ stk' = F' s stk)
        (cfs ! 0) (cfs ! (length cfs - 1))"
      (is "⋀cfs. _ ⟹ ?Q' x' (cfs ! 0) (cfs ! (length cfs - 1))") and
    D: "I (fst (snd (cfs ! 0))) = 0"
  shows "∃k < length cfs. ∃t. (λ(pc, s, stk) (pc', s', stk').
    pc = 0 ∧ pc' = size (P x) + size (P' x') + I' t ∧ Q s t ∧ Q' t s' ∧
      stk' = F' t (F s stk)) (cfs ! 0) (cfs ! k)"
by (subgoal_tac "[] @ ?P ⊨ cfs□", drule execl_all_sub [where k = 0 and Q = ?Q],
 insert A B, (clarsimp simp: execl_all_def)+, insert A C D, drule execl_all_sub
 [where Q = ?Q'], simp+, clarify, rule exI, rule conjI, simp, rule exI, auto)

lemma execl_all_sub_m [rule_format]:
  assumes
    A: "P @ P' x @ P'' ⊨ cfs□" and
    B: "k < length cfs" and
    C: "fst (cfs ! k) = size P" and
    D: "length (snd (snd (cfs ! 0))) ≤ length (snd (snd (cfs ! k)))" and
    E: "∀cfs. P' x ⊨ cfs□ ⟶ Q x (cfs ! 0) (cfs ! (length cfs - 1))" and
    F: "∀cfs. P' x ⊨ cfs□ ⟶ mpred (P' x) cfs 0 (length cfs - 1)"
  shows "∃k' < length cfs. Q x (off P (cfs ! k)) (off P (cfs ! k')) ∧
    mpred (P @ P' x @ P'') cfs k k'"
proof -
  have "∃k' ∈ {k..<length cfs}. P' x ⊨ map (off P) (drop k (take (Suc k') cfs))□"
    (is "∃k' ∈ _. _ ⊨ ?F k'□")
    using A and B and C by (rule execl_all)
  then obtain k' where G: "k' ∈ {k..<length cfs}" and H: "P' x ⊨ ?F k'□" and
   "Q x (?F k' ! 0) (?F k' ! (length (?F k') - 1))"
    using E by blast
  moreover from this have "?F k' ! (length (?F k') - 1) = off P (cfs ! k')"
    by (auto dest!: min_absorb2 simp: less_eq_Suc_le)
  ultimately have I: "Q x (off P (cfs ! k)) (off P (cfs ! k'))"
    by auto
  have "mpred (P' x) (?F k') 0 (length (?F k') - 1)"
    using F and H by blast
  moreover have "length (?F k') - 1 = k' - k"
    using G by auto
  ultimately have "mpred (P @ P' x @ P'') cfs k k'"
  proof (auto del: conjI simp: mpred_def split: prod.split prod.split_asm)
    fix j s stk pc0 s0 stk0 pc' s' stk'
    assume "∀j' ∈ {0..<k' - k}. ∀s' stk'. snd (cfs ! (k + j')) = (s', stk') ⟶
      msp (P' x) (fst (cfs ! (k + j')) - size P) ≤ length stk' - length stk ∧
      length stk ≤ length stk'" and
      J: "k ≤ j" and
      K: "j < k'" and
      L: "cfs ! 0 = (pc0, s0, stk0)" and
      M: "snd (cfs ! k) = (s, stk)" and
      N: "cfs ! j = (pc', s', stk')"
    moreover from this have "snd (cfs ! (k + (j - k))) = (s', stk')"
      by simp
    ultimately have "msp (P' x) (pc' - size P) ≤ length stk' - length stk ∧
      length stk ≤ length stk'"
      by fastforce
    moreover have "0 ≤ pc' - size P ∧ pc' - size P < size (P' x)"
      using G and H and J and K and N by (insert execl_next
       [of "P' x" "?F k'" "j - k"], simp add: execl_all_def)
    ultimately show "msp (P @ P' x @ P'') pc' ≤ length stk' - length stk0 ∧
      length stk0 ≤ length stk'"
      using D and L and M by (auto simp: msp_def split: instr.split)
  qed
  thus ?thesis
    using G and I by auto
qed

text ‹
\null

The lemmas here below establish the properties of predicate @{const mpred} required for the new
well-behavedness proof. In more detail:

  ▪ Lemma @{text mpred_merge} states that, if two consecutive sublists of a list of configurations
    are both well-behaved, then such is the merged sublist. This lemma is the means enabling to
    infer that a complete execution made of well-behaved pieces is itself well-behaved.

  ▪ Lemma @{text mpred_drop} states that, under proper assumptions, if a sublist of a suffix of a
    list of configurations is well-behaved, then such is the matching sublist of the whole list. In
    the subgoal of the well-behavedness proof for loops where an iteration has been run, this lemma
    can be used to deduce the well-behavedness of the whole execution from that of the sub-execution
    following that iteration.

  ▪ Lemma @{text mpred_execl_m_exec} states that, if a nonempty small-step assembly code execution
    is well-behaved, then the machine configurations corresponding to the initial and final assembly
    ones are linked by a machine code execution. Namely, this lemma proves that the well-behavedness
    property expressed by predicate @{const mpred} is sufficient to fulfill the assumptions of lemma
    @{thm [source] exec1_m_exec1} in each intermediate step. Once any complete small-step assembly
    program execution is proven to satisfy @{const mpred}, this lemma can then be used to achieve
    the final goal of establishing that source programs are simulated by machine ones.

\null
›

lemma mpred_merge:
 "⟦mpred P cfs k m; mpred P cfs m n⟧ ⟹ mpred P cfs k n"
by (subgoal_tac "{k..<n} ⊆ {k..<m} ∪ {m..<n}",
 simp add: mpred_def split: prod.split_asm, rule ballI, auto)

lemma mpred_drop:
  assumes
    A: "k ≤ length cfs" and
    B: "length (snd (snd (cfs ! 0))) ≤ length (snd (snd (cfs ! k)))"
  shows "mpred P (drop k cfs) m n ⟹ mpred P cfs (k + m) (k + n)"
proof (clarsimp simp: mpred_def)
  fix k' pc pc' pc'' s s' s'' stk stk'' and stk' :: stack
  assume "∀k'' ∈ {m..<n}. case drop k cfs ! k'' of (pc'', s'', stk'') ⇒
    msp P pc'' ≤ length stk'' - length stk' ∧ length stk' ≤ length stk''"
    (is "∀k'' ∈ _. ?Q k''")
  hence "k' - k ∈ {m..<n} ⟶ ?Q (k' - k)"
    by simp
  moreover assume "k + m ≤ k'" and "k' < k + n" and "cfs ! 0 = (pc, s, stk)" and
   "drop k cfs ! 0 = (pc', s', stk')" and "cfs ! k' = (pc'', s'', stk'')"
  ultimately show
   "msp P pc'' ≤ length stk'' - length stk ∧ length stk ≤ length stk''"
    using A and B by auto
qed

lemma mpred_execl_m_exec [simplified Let_def]:
 "⟦cfs ≠ []; P ⊨ cfs; mpred P cfs 0 (length cfs - 1)⟧ ⟹
    case (cfs ! 0, cfs ! (length cfs - 1)) of ((pc, s, stk), (pc', s', stk')) ⇒
      let sp' = length stk' - length stk in to_m_prog P ⊢
        (pc, to_m_state (vars P) s, 0) →*
        (pc', add_m_stack sp' stk' (to_m_state (vars P) s'), sp')"
proof (induction cfs rule: rev_nonempty_induct, force, rule rev_cases, erule notE,
 simp_all only: nth_append, auto simp: Let_def simp del: to_m_prog.simps)
  fix cfs pc pc' pc'' s s' s'' stk'' and stk :: stack and stk' :: stack
  let ?sp = "length stk' - length stk"
  assume "P ⊨ cfs @ [(pc', s', stk')] ⟹
    mpred P (cfs @ [(pc', s', stk')]) 0 (length cfs) ⟹
      to_m_prog P ⊢
        (pc, to_m_state (vars P) s, 0) →*
        (pc', add_m_stack ?sp stk' (to_m_state (vars P) s'), ?sp)"
    (is "?P ⟹ ?Q ⟹ ?R")
  moreover assume A: "P ⊨ cfs @ [(pc', s', stk'), (pc'', s'', stk'')]"
    (is "_ ⊨ ?cfs")
  hence ?P
    by (drule_tac execl_take [where n = "Suc (length cfs)"], simp)
  moreover assume B: "mpred P ?cfs 0 (Suc (length cfs))"
  hence ?Q
    by (auto simp: mpred_def nth_append split: if_split_asm)
  ultimately have ?R
    by simp
  let ?sp' = "?sp + length stk'' - length stk'"
  let ?sp'' = "length stk'' - length stk"
  have "P ⊢ (pc', s', stk') → (pc'', s'', stk'')"
    by (insert execl_drop [OF A, of "length cfs"], simp)
  moreover assume "(cfs @ [(pc', s', stk')]) ! 0 = (pc, s, stk)"
  hence C: "msp P pc' ≤ ?sp ∧ length stk ≤ length stk'"
    using B by (auto simp: mpred_def nth_append split: if_split_asm)
  ultimately have "to_m_prog P ⊢
    (pc', add_m_stack ?sp stk' (to_m_state (vars P) s'), ?sp) →
    (pc'', add_m_stack ?sp' stk'' (to_m_state (vars P) s''), ?sp')"
    by (rule_tac exec1_m_exec1, simp_all)
  thus "to_m_prog P ⊢
    (pc, to_m_state (vars P) s, 0) →*
    (pc'', add_m_stack ?sp'' stk'' (to_m_state (vars P) s''), ?sp'')"
    using `?R` and C by (auto intro: star_trans)
qed


subsection "Main theorems"

text ‹
Here below is the proof that every complete small-step execution of an assembly program fulfills
predicate @{const cpred} (lemma @{text ccomp_correct}), which is reused as is from cite‹"Noce21"›,
followed by the proof that every such execution satisfies predicate @{const mpred} as well (lemma
@{text ccomp_correct_m}), which closely resembles the former one.

\null
›

lemma acomp_acomp:
 "⟦acomp a1 @ acomp a2 @ P ⊨ cfs□;
    ⋀cfs. acomp a1 ⊨ cfs□ ⟹ apred a1 (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. acomp a2 ⊨ cfs□ ⟹ apred a2 (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (∃k < length cfs. cfs ! k =
    (size (acomp a1 @ acomp a2), s, aval a2 s # aval a1 s # stk))"
by (drule execl_all_sub2 [where I = "λs. 0" and I' = "λs. 0" and Q = "λs s'. s' = s"
 and Q' = "λs s'. s' = s" and F = "λs stk. aval a1 s # stk"
 and F' = "λs stk. aval a2 s # stk"], auto simp: apred_def)

lemma bcomp_bcomp:
 "⟦bcomp (b1, f1, i1) @ bcomp (b2, f2, i2) ⊨ cfs□;
    ⋀cfs. bcomp (b1, f1, i1) ⊨ cfs□ ⟹
      bpred (b1, f1, i1) (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. bcomp (b2, f2, i2) ⊨ cfs□ ⟹
      bpred (b2, f2, i2) (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (bval b1 s ≠ f1 ⟶
    (∃k < length cfs. cfs ! k = (size (bcomp (b1, f1, i1) @ bcomp (b2, f2, i2)) +
      (if bval b2 s = f2 then i2 else 0), s, stk)))"
by (clarify, rule conjI, simp add: execl_all_def, rule impI, subst (asm) append_Nil2
 [symmetric], drule execl_all_sub2 [where I = "λs. if bval b1 s = f1 then i1 else 0"
 and I' = "λs. if bval b2 s = f2 then i2 else 0" and Q = "λs s'. s' = s"
 and Q' = "λs s'. s' = s" and F = "λs stk. stk" and F' = "λs stk. stk"],
 auto simp: bpred_def)

lemma acomp_correct [simplified, intro]:
 "acomp a ⊨ cfs□ ⟹ apred a (cfs ! 0) (cfs ! (length cfs - 1))"
proof (induction a arbitrary: cfs, simp_all, frule_tac [3] acomp_acomp, auto)
  fix a1 a2 cfs s stk k
  assume A: "acomp a1 @ acomp a2 @ [ADD] ⊨ cfs□"
    (is "?ca1 @ ?ca2 @ ?i ⊨ _□")
  assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca1 + size ?ca2, s, aval a2 s # aval a1 s # stk)"
  hence "cfs ! Suc k = (size (?ca1 @ ?ca2 @ ?i), s, aval (Plus a1 a2) s # stk)"
    using A by (insert execl_next [of "?ca1 @ ?ca2 @ ?i" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  thus "apred (Plus a1 a2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and B and C by (insert execl_last [of "?ca1 @ ?ca2 @ ?i" cfs "Suc k"],
     simp add: execl_all_def apred_def, drule_tac impI, auto)
qed

lemma bcomp_correct [simplified, intro]:
 "⟦bcomp x ⊨ cfs□; 0 ≤ snd (snd x)⟧ ⟹ bpred x (cfs ! 0) (cfs ! (length cfs - 1))"
proof (induction x arbitrary: cfs rule: bcomp.induct, simp_all add: Let_def,
 frule_tac [4] acomp_acomp, frule_tac [3] bcomp_bcomp, auto, force simp: bpred_def)
  fix b1 b2 f i cfs s stk
  assume A: "bcomp (b1, False, size (bcomp (b2, f, i)) + (if f then 0 else i)) @
    bcomp (b2, f, i) ⊨ cfs□"
    (is "bcomp (_, _, ?n + ?i) @ ?cb ⊨ _□")
  moreover assume B: "cfs ! 0 = (0, s, stk)" and
   "⋀cb cfs. ⟦cb = ?cb; bcomp (b1, False, ?n + ?i) ⊨ cfs□⟧ ⟹
      bpred (b1, False, ?n + ?i) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  ultimately have "∃k < length cfs. bpred (b1, False, ?n + ?i)
    (off [] (cfs ! 0)) (off [] (cfs ! k))"
    by (rule_tac execl_all_sub, auto simp: execl_all_def)
  moreover assume C: "¬ bval b1 s"
  ultimately obtain k where D: "k < length cfs" and
    E: "cfs ! k = (size (bcomp (b1, False, ?n + ?i)) + ?n + ?i, s, stk)"
    using B by (auto simp: bpred_def)
  assume "0 ≤ i"
  thus "bpred (And b1 b2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and C and D and E by (insert execl_last, auto simp:
     execl_all_def bpred_def Let_def)
next
  fix b1 b2 f i cfs s stk k
  assume A: "bcomp (b1, False, size (bcomp (b2, f, i)) + (if f then 0 else i)) @
    bcomp (b2, f, i) ⊨ cfs□"
    (is "?cb1 @ ?cb2 ⊨ _□")
  assume "k < length cfs" and "0 ≤ i" and "bval b1 s" and
   "cfs ! k = (size ?cb1 + size ?cb2 + (if bval b2 s = f then i else 0), s, stk)"
  thus "bpred (And b1 b2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A by (insert execl_last, auto simp: execl_all_def bpred_def Let_def)
next
  fix a1 a2 f i cfs s stk k
  assume A: "acomp a1 @ acomp a2 @
    (if f then [JMPLESS i] else [JMPGE i]) ⊨ cfs□"
    (is "?ca1 @ ?ca2 @ ?i ⊨ _□")
  assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca1 + size ?ca2, s, aval a2 s # aval a1 s # stk)"
  hence D: "cfs ! Suc k =
    (size (?ca1 @ ?ca2 @ ?i) + (if bval (Less a1 a2) s = f then i else 0), s, stk)"
    using A by (insert execl_next [of "?ca1 @ ?ca2 @ ?i" cfs k],
     simp add: execl_all_def, drule_tac impI, auto split: if_split_asm)
  assume "0 ≤ i"
  with A and B and C and D have "length cfs - 1 = Suc k"
    by (rule_tac execl_last, auto simp: execl_all_def, simp split: if_split_asm)
  thus "bpred (Less a1 a2, f, i) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using D by (simp add: bpred_def)
qed


lemma bcomp_ccomp:
 "⟦bcomp (b, f, i) @ ccomp c @ P ⊨ cfs□; 0 ≤ i;
    ⋀cfs. ccomp c ⊨ cfs□ ⟹ cpred c (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (bval b s ≠ f ⟶
    (∃k < length cfs. case cfs ! k of (pc', s', stk') ⇒
      pc' = size (bcomp (b, f, i) @ ccomp c) ∧ (c, s) ⇒ s' ∧ stk' = stk))"
by (clarify, rule conjI, simp add: execl_all_def, rule impI, drule execl_all_sub2
 [where I = "λs. if bval b s = f then i else 0" and I' = "λs. 0"
 and Q = "λs s'. s' = s" and Q' = "λs s'. (c, s) ⇒ s'" and F = "λs stk. stk"
 and F' = "λs stk. stk"], insert bcomp_correct [of "(b, f, i)"],
 auto simp: bpred_def cpred_def)

lemma ccomp_ccomp:
 "⟦ccomp c1 @ ccomp c2 ⊨ cfs□;
    ⋀cfs. ccomp c1 ⊨ cfs□ ⟹ cpred c1 (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. ccomp c2 ⊨ cfs□ ⟹ cpred c2 (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (∃k < length cfs. ∃t.
    case cfs ! k of (pc', s', stk') ⇒ pc' = size (ccomp c1 @ ccomp c2) ∧
      (c1, s) ⇒ t ∧ (c2, t) ⇒ s' ∧ stk' = stk)"
by (subst (asm) append_Nil2 [symmetric], drule execl_all_sub2 [where I = "λs. 0"
 and I' = "λs. 0" and Q = "λs s'. (c1, s) ⇒ s'" and Q' = "λs s'. (c2, s) ⇒ s'"
 and F = "λs stk. stk" and F' = "λs stk. stk"], auto simp: cpred_def, force)

lemma while_correct [simplified, intro]:
 "⟦bcomp (b, False, size (ccomp c) + 1) @ ccomp c @
    [JMP (- (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1))]
      ⊨ cfs□;
    ⋀cfs. ccomp c ⊨ cfs□ ⟹ cpred c (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  cpred (WHILE b DO c) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  (is "⟦?cb @ ?cc @ [JMP (- ?n)] ⊨ _□; ⋀_. _ ⟹ _⟧ ⟹ ?Q cfs")
proof (induction cfs rule: length_induct, frule bcomp_ccomp, auto)
  fix cfs s stk
  assume A: "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] ⊨ cfs□"
  hence "∃k < length cfs. bpred (b, False, size (ccomp c) + 1)
    (off [] (cfs ! 0)) (off [] (cfs ! k))"
    by (rule_tac execl_all_sub, auto simp: execl_all_def)
  moreover assume B: "¬ bval b s" and "cfs ! 0 = (0, s, stk)"
  ultimately obtain k where "k < length cfs" and "cfs ! k = (?n, s, stk)"
    by (auto simp: bpred_def)
  thus "cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and B by (insert execl_last, auto simp: execl_all_def cpred_def Let_def)
next
  fix cfs s s' stk k
  assume A: "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] ⊨ cfs□"
    (is "?P ⊨ _□")
  assume B: "k < length cfs" and "cfs ! k = (size ?cb + size ?cc, s', stk)"
  moreover from this have C: "k ≠ length cfs - 1"
    using A by (rule_tac notI, simp add: execl_all_def)
  ultimately have D: "cfs ! Suc k = (0, s', stk)"
    using A by (insert execl_next [of ?P cfs k], auto simp: execl_all_def)
  moreover have E: "Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1"
    (is "_ + (length ?cfs - _) = _")
    using B and C by simp
  ultimately have "?P ⊨ ?cfs□"
    using A and B and C by (auto simp: execl_all_def intro: execl_drop)
  moreover assume "∀cfs'. length cfs' < length cfs ⟶ ?P ⊨ cfs'□ ⟶ ?Q cfs'"
  hence "length ?cfs < length cfs ⟶ ?P ⊨ ?cfs□ ⟶ ?Q ?cfs" ..
  ultimately have "cpred (WHILE b DO c) (cfs ! Suc k) (cfs ! (length cfs - 1))"
    using B and C and E by simp
  moreover assume "bval b s" and "(c, s) ⇒ s'"
  ultimately show "cpred (WHILE b DO c) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using D by (auto simp: cpred_def)
qed

lemma ccomp_correct [simplified, intro]:
 "ccomp c ⊨ cfs□ ⟹ cpred c (cfs ! 0) (cfs ! (length cfs - 1))"
proof (induction c arbitrary: cfs, simp_all add: Let_def, frule_tac [4] bcomp_ccomp,
 frule_tac [3] ccomp_ccomp, auto)
  fix a x cfs
  assume A: "acomp a @ [STORE x] ⊨ cfs□"
  hence "∃k < length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k))"
    by (rule_tac execl_all_sub, auto simp: execl_all_def)
  moreover obtain s stk where B: "cfs ! 0 = (0, s, stk)"
    using A by (cases "cfs ! 0", simp add: execl_all_def)
  ultimately obtain k where C: "k < length cfs" and
    D: "cfs ! k = (size (acomp a), s, aval a s # stk)"
    by (auto simp: apred_def)
  hence "cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)"
    using A by (insert execl_next [of "acomp a @ [STORE x]" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  thus "cpred (x ::= a) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
    using A and B and C and D by (insert execl_last [of "acomp a @ [STORE x]"
     cfs "Suc k"], simp add: execl_all_def cpred_def, drule_tac impI, auto)
next
  fix c1 c2 cfs s s' t stk k
  assume "ccomp c1 @ ccomp c2 ⊨ cfs□" and "k < length cfs" and
   "cfs ! k = (size (ccomp c1) + size (ccomp c2), s', stk)"
  moreover assume "(c1, s) ⇒ t" and "(c2, t) ⇒ s'"
  ultimately show "cpred (c1;; c2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    by (insert execl_last, auto simp: execl_all_def cpred_def)
next
  fix b c1 c2 cfs s stk
  assume A: "bcomp (b, False, size (ccomp c1) + 1) @ ccomp c1 @
    JMP (size (ccomp c2)) # ccomp c2 ⊨ cfs□"
    (is "bcomp ?x @ ?cc1 @ _ # ?cc2 ⊨ _□")
  let ?P = "bcomp ?x @ ?cc1 @ [JMP (size ?cc2)]"
  have "∃k < length cfs. bpred ?x (off [] (cfs ! 0)) (off [] (cfs ! k))"
    using A by (rule_tac execl_all_sub, auto simp: execl_all_def)
  moreover assume B: "¬ bval b s" and "cfs ! 0 = (0, s, stk)"
  ultimately obtain k where C: "k < length cfs" and D: "cfs ! k = (size ?P, s, stk)"
    by (force simp: bpred_def)
  assume "⋀cfs. ?cc2 ⊨ cfs□ ⟹ cpred c2 (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  hence "∃k' < length cfs. cpred c2 (off ?P (cfs ! k)) (off ?P (cfs ! k'))"
    using A and C and D by (rule_tac execl_all_sub [where P'' = "[]"], auto)
  then obtain k' where "k' < length cfs" and "case cfs ! k' of (pc', s', stk') ⇒
    pc' = size (?P @ ?cc2) ∧ (c2, s) ⇒ s' ∧ stk' = stk"
    using D by (fastforce simp: cpred_def)
  thus "cpred (IF b THEN c1 ELSE c2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and B by (insert execl_last, auto simp: execl_all_def cpred_def Let_def)
next
  fix b c1 c2 cfs s s' stk k
  assume A: "bcomp (b, False, size (ccomp c1) + 1) @ ccomp c1 @
    JMP (size (ccomp c2)) # ccomp c2 ⊨ cfs□"
    (is "?cb @ ?cc1 @ ?i # ?cc2 ⊨ _□")
  assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc1, s', stk)"
  hence D: "cfs ! Suc k = (size (?cb @ ?cc1 @ ?i # ?cc2), s', stk)"
    (is "_ = (size ?P, _, _)")
    using A by (insert execl_next [of ?P cfs k], simp add: execl_all_def,
     drule_tac impI, auto)
  assume "bval b s" and "(c1, s) ⇒ s'"
  thus "cpred (IF b THEN c1 ELSE c2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and B and C and D by (insert execl_last [of ?P cfs "Suc k"],
     simp add: execl_all_def cpred_def Let_def, drule_tac impI, auto)
qed


lemma acomp_acomp_m:
  assumes
    A: "acomp a1 @ acomp a2 @ P ⊨ cfs□"
      (is "?P ⊨ _□") and
    B: "⋀cfs. acomp a1 ⊨ cfs□ ⟹ mpred (acomp a1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. acomp a2 ⊨ cfs□ ⟹ mpred (acomp a2) cfs 0 (length cfs - 1)"
  shows "case cfs ! 0 of (pc, s, stk) ⇒ ∃k < length cfs.
    cfs ! k = (size (acomp a1 @ acomp a2), s, aval a2 s # aval a1 s # stk) ∧
    mpred ?P cfs 0 k"
proof -
  have "∃k < length cfs. apred a1 (off [] (cfs ! 0)) (off [] (cfs ! k)) ∧
    mpred ([] @ ?P) cfs 0 k"
    using A and B by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k s stk where
   "cfs ! 0 = (0, s, stk) ∧ mpred ?P cfs 0 k ∧ k < length cfs" and
    D: "cfs ! k = (size (acomp a1), s, aval a1 s # stk)"
    using A by (auto simp: apred_def execl_all_def)
  moreover from this have "∃k' < length cfs. apred a2 (off (acomp a1) (cfs ! k))
    (off (acomp a1) (cfs ! k')) ∧ mpred ?P cfs k k'"
    using A and C by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k' where "k' < length cfs ∧ mpred ?P cfs k k' ∧
    cfs ! k' = (size (acomp a1 @ acomp a2), s, aval a2 s # aval a1 s # stk)"
    using D by (fastforce simp: apred_def prod_eq_iff)
  ultimately show ?thesis
    by (auto intro: mpred_merge)
qed

lemma bcomp_bcomp_m [simplified, intro]:
  assumes A: "bcomp (b1, f1, i1) @ bcomp (b2, f2, i2) ⊨ cfs□"
    (is "bcomp ?x1 @ bcomp ?x2 ⊨ _□")
  assumes
    B: "⋀cfs. bcomp ?x1 ⊨ cfs□ ⟹ mpred (bcomp ?x1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. bcomp ?x2 ⊨ cfs□ ⟹ mpred (bcomp ?x2) cfs 0 (length cfs - 1)" and
    D: "size (bcomp ?x2) ≤ i1" and
    E: "0 ≤ i2"
  shows "mpred (bcomp ?x1 @ bcomp ?x2) cfs 0 (length cfs - 1)"
    (is "mpred ?P _ _ _")
proof -
  have "∃k < length cfs. bpred ?x1 (off [] (cfs ! 0)) (off [] (cfs ! k)) ∧
    mpred ([] @ ?P) cfs 0 k"
    using A and B and D by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k s stk where
   "cfs ! 0 = (0, s, stk) ∧ mpred ?P cfs 0 k ∧ k < length cfs" and
    F: "cfs ! k = (size (bcomp ?x1) + (if bval b1 s = f1 then i1 else 0), s, stk)"
    using A by (auto simp: bpred_def execl_all_def)
  moreover from this have "bval b1 s ≠ f1 ⟹ ∃k' < length cfs.
    bpred ?x2 (off (bcomp ?x1) (cfs ! k)) (off (bcomp ?x1) (cfs ! k')) ∧
    mpred (bcomp ?x1 @ bcomp ?x2 @ []) cfs k k'"
    using A and C and E by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k' where "bval b1 s ≠ f1 ⟹ k' < length cfs ∧ mpred ?P cfs k k' ∧
    fst (cfs ! k') = size ?P + (if bval b2 s = f2 then i2 else 0)"
    using F by (fastforce simp: bpred_def)
  ultimately have "∃k < length cfs. fst (cfs ! k) = (if bval b1 s = f1 then
    size (bcomp ?x1) + i1 else size ?P + (if bval b2 s = f2 then i2 else 0)) ∧
    mpred ?P cfs 0 k"
    (is "∃k < _. ?Q k")
    by (fastforce intro: mpred_merge)
  then obtain k'' where "k'' < length cfs ∧ ?Q k''" ..
  with A and D and E show ?thesis
    by (insert execl_last [of ?P cfs k''], simp add: execl_all_def)
qed

lemma acomp_correct_m [simplified, intro]:
 "acomp a ⊨ cfs□ ⟹ mpred (acomp a) cfs 0 (length cfs - 1)"
proof (induction a arbitrary: cfs, (fastforce simp: mpred_def msp_def)+, simp,
 frule acomp_acomp_m, auto)
  fix a1 a2 cfs pc s stk k
  assume A: "acomp a1 @ acomp a2 @ [ADD] ⊨ cfs□"
    (is "?P ⊨ _□")
  assume "cfs ! 0 = (pc, s, stk)" and "mpred ?P cfs 0 k" and
    B: "k < length cfs" and 
    C: "cfs ! k = (size (acomp a1) + size (acomp a2), s,
      aval a2 s # aval a1 s # stk)"
  moreover from this have "mpred ?P cfs k (Suc k)"
    by (simp add: mpred_def msp_def)
  moreover have "cfs ! Suc k = (size ?P, s, aval (Plus a1 a2) s # stk)"
    using A and B and C by (insert execl_next [of ?P cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    using A by (insert execl_last [of ?P cfs "Suc k"], simp add: execl_all_def,
     drule_tac impI, auto intro: mpred_merge)
qed

lemma bcomp_correct_m [simplified, intro]:
 "⟦bcomp x ⊨ cfs□; 0 ≤ snd (snd x)⟧ ⟹ mpred (bcomp x) cfs 0 (length cfs - 1)"
proof (induction x arbitrary: cfs rule: bcomp.induct, force simp: mpred_def msp_def,
 (simp add: Let_def)+, fastforce, subst (asm) bcomp.simps, frule acomp_acomp_m,
 auto simp del: bcomp.simps, subst bcomp.simps)
  fix a1 a2 f i cfs pc s stk k
  assume A: "acomp a1 @ acomp a2 @
    (if f then [JMPLESS i] else [JMPGE i]) ⊨ cfs□"
    (is "?P ⊨ _□")
  assume "cfs ! 0 = (pc, s, stk)" and "mpred ?P cfs 0 k" and
    B: "k < length cfs" and 
    C: "cfs ! k = (size (acomp a1) + size (acomp a2), s,
      aval a2 s # aval a1 s # stk)"
  moreover from this have "mpred ?P cfs k (Suc k)"
    by (simp add: mpred_def msp_def)
  moreover from this have D: "cfs ! Suc k =
    (size ?P + (if bval (Less a1 a2) s = f then i else 0), s, stk)"
    using A and B and C by (insert execl_next [of ?P cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  assume "0 ≤ i"
  with A and B and C and D have "length cfs - 1 = Suc k"
    by (rule_tac execl_last, auto simp: execl_all_def, simp split: if_split_asm)
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    by (auto intro: mpred_merge)
qed


lemma bcomp_ccomp_m:
  assumes A: "bcomp (b, f, i) @ ccomp c @ P ⊨ cfs□"
    (is "bcomp ?x @ ?cc @ _ ⊨ _□")
  assumes
    B: "⋀cfs. ?cc ⊨ cfs□ ⟹ mpred ?cc cfs 0 (length cfs - 1)" and
    C: "0 ≤ i"
  shows "case cfs ! 0 of (pc, s, stk) ⇒ ∃k < length cfs. ∃s'.
    cfs ! k = (size (bcomp ?x) + (if bval b s = f then i else size ?cc), s', stk) ∧
    mpred (bcomp ?x @ ?cc @ P) cfs 0 k"
proof -
  let ?P = "bcomp ?x @ ?cc @ P"
  have "∃k < length cfs. bpred ?x (off [] (cfs ! 0)) (off [] (cfs ! k)) ∧
    mpred ([] @ ?P) cfs 0 k"
    using A and C by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain s stk k where
   "cfs ! 0 = (0, s, stk) ∧ mpred ?P cfs 0 k ∧ k < length cfs" and
    D: "cfs ! k = (size (bcomp ?x) + (if bval b s = f then i else 0), s, stk)"
    using A by (auto simp: bpred_def execl_all_def)
  moreover from this have "bval b s ≠ f ⟹ ∃k' < length cfs. cpred c
    (off (bcomp ?x) (cfs ! k)) (off (bcomp ?x) (cfs ! k')) ∧ mpred ?P cfs k k'"
    using A and B by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k' s' where "bval b s ≠ f ⟹ k' < length cfs ∧ mpred ?P cfs k k' ∧
    cfs ! k' = (size (bcomp ?x @ ?cc), s', stk)"
    using D by (fastforce simp: cpred_def prod_eq_iff)
  ultimately show ?thesis
    by (auto intro: mpred_merge)
qed

lemma ccomp_ccomp_m [simplified, intro]:
  assumes
    A: "ccomp c1 @ ccomp c2 ⊨ cfs□"
      (is "?P ⊨ _□") and
    B: "⋀cfs. ccomp c1 ⊨ cfs□ ⟹ mpred (ccomp c1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. ccomp c2 ⊨ cfs□ ⟹ mpred (ccomp c2) cfs 0 (length cfs - 1)"
  shows "mpred ?P cfs 0 (length cfs - 1)"
proof -
  have "∃k < length cfs. cpred c1 (off [] (cfs ! 0)) (off [] (cfs ! k)) ∧
    mpred ([] @ ?P) cfs 0 k"
    using A and B by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k s s' stk where
   "cfs ! 0 = (0, s, stk) ∧ mpred ?P cfs 0 k ∧ k < length cfs" and
    D: "cfs ! k = (size (ccomp c1), s', stk)"
    using A by (auto simp: cpred_def execl_all_def)
  moreover from this have "∃k' < length cfs. cpred c2 (off (ccomp c1) (cfs ! k))
    (off (ccomp c1) (cfs ! k')) ∧ mpred (ccomp c1 @ ccomp c2 @ []) cfs k k'"
    using A and C by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k' where
   "fst (cfs ! k') = size ?P ∧ mpred ?P cfs k k' ∧ k' < length cfs"
    using D by (fastforce simp: cpred_def)
  ultimately show ?thesis
    using A by (insert execl_last [of ?P cfs k'], simp add: execl_all_def,
     auto intro: mpred_merge)
qed

lemma while_correct_m [simplified, simplified Let_def, intro]:
 "⟦bcomp (b, False, size (ccomp c) + 1) @ ccomp c @
    [JMP (- (size (bcomp (b, False, size (ccomp c) + 1) @ ccomp c) + 1))]
      ⊨ cfs□;
    ⋀cfs. ccomp c ⊨ cfs□ ⟹ mpred (ccomp c) cfs 0 (length cfs - 1)⟧ ⟹
  mpred (ccomp (WHILE b DO c)) cfs 0 (length cfs - Suc 0)"
  (is "⟦?cb @ ?cc @ _ ⊨ _□; ⋀_. _ ⟹ _⟧ ⟹ _")
proof (induction cfs rule: length_induct, frule bcomp_ccomp_m,
 auto simp: Let_def split: if_split_asm)
  fix cfs s stk k
  assume "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] ⊨ cfs□"
    (is "?P ⊨ _□")
  moreover assume "mpred ?P cfs 0 k" and "k < length cfs" and
   "cfs ! k = (size ?cb + (size ?cc + 1), s, stk)"
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    by (insert execl_last [of ?P cfs k], simp add: execl_all_def)
next
  fix cfs pc s s' stk k
  assume A: "?cb @ ?cc @ [JMP (- size ?cb - size ?cc - 1)] ⊨ cfs□"
    (is "?P ⊨ _□")
  assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc, s', stk)"
  moreover from this have D: "k ≠ length cfs - 1"
    using A by (rule_tac notI, simp add: execl_all_def)
  ultimately have E: "cfs ! Suc k = (0, s', stk)"
    using A by (insert execl_next [of ?P cfs k], auto simp: execl_all_def)
  moreover have F: "Suc k + (length (drop (Suc k) cfs) - 1) = length cfs - 1"
    (is "_ + (length ?cfs - _) = _")
    using B and D by simp
  ultimately have "?P ⊨ ?cfs□"
    using A and B and D by (auto simp: execl_all_def intro: execl_drop)
  moreover assume "∀cfs'. length cfs' < length cfs ⟶ ?P ⊨ cfs'□ ⟶
    mpred ?P cfs' 0 (length cfs' - Suc 0)"
  ultimately have "mpred ?P ?cfs 0 (length ?cfs - 1)"
    using B by force
  moreover assume G: "cfs ! 0 = (pc, s, stk)"
  ultimately have "mpred ?P cfs (Suc k + 0) (Suc k + (length ?cfs - 1))"
    using B and E by (rule_tac mpred_drop, simp_all)
  hence "mpred ?P cfs (Suc k) (length cfs - 1)"
    by (subst (asm) F, simp)
  moreover assume "mpred ?P cfs 0 k"
  moreover have "mpred ?P cfs k (Suc k)"
    using C and G by (simp add: mpred_def msp_def)
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    by (auto intro: mpred_merge)
qed

lemma ccomp_correct_m:
 "ccomp c ⊨ cfs□ ⟹ mpred (ccomp c) cfs 0 (length cfs - 1)"
proof (induction c arbitrary: cfs, (fastforce simp: mpred_def)+,
 simp_all add: Let_def, frule_tac [3] bcomp_ccomp_m, auto split: if_split_asm)
  fix a x cfs
  assume A: "acomp a @ [STORE x] ⊨ cfs□"
    (is "?P ⊨ _□")
  hence "∃k < length cfs. apred a (off [] (cfs ! 0)) (off [] (cfs ! k)) ∧
    mpred ([] @ ?P) cfs 0 k"
    by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k s stk where "cfs ! 0 = (0, s, stk) ∧ mpred ?P cfs 0 k" and
    B: "k < length cfs ∧ cfs ! k = (size (acomp a), s, aval a s # stk)"
    using A by (auto simp: apred_def execl_all_def)
  moreover from this have "mpred ?P cfs k (Suc k)"
    by (simp add: mpred_def msp_def)
  moreover have "cfs ! Suc k = (size (acomp a) + 1, s(x := aval a s), stk)"
    using A and B by (insert execl_next [of "acomp a @ [STORE x]" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    using A by (insert execl_last [of ?P cfs "Suc k"], simp add: execl_all_def,
     drule_tac impI, auto intro: mpred_merge)
next
  fix b c1 c2 cfs pc s s' stk k
  assume A: "bcomp (b, False, size (ccomp c1) + 1) @ ccomp c1 @
    JMP (size (ccomp c2)) # ccomp c2 ⊨ cfs□"
    (is "?cb @ ?cc1 @ ?i # ?cc2 ⊨ _□")
  let ?P = "?cb @ ?cc1 @ [?i]"
  assume B: "cfs ! k = (size ?cb + (size ?cc1 + 1), s', stk)"
  assume "cfs ! 0 = (pc, s, stk)" and "k < length cfs" and
   "⋀cfs. ?cc2 ⊨ cfs□ ⟹ mpred ?cc2 cfs 0 (length cfs - Suc 0)"
  hence "∃k' < length cfs. cpred c2 (off ?P (cfs ! k)) (off ?P (cfs ! k')) ∧
    mpred (?P @ ?cc2 @ []) cfs k k'"
    using A and B by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
  then obtain k' where "fst (cfs ! k') = size (?P @ ?cc2) ∧
    mpred (?P @ ?cc2) cfs k k' ∧ k' < length cfs"
    using B by (fastforce simp: cpred_def)
  moreover assume "mpred (?cb @ ?cc1 @ ?i # ?cc2) cfs 0 k"
  ultimately show "mpred (?cb @ ?cc1 @ ?i # ?cc2) cfs 0 (length cfs - Suc 0)"
    using A by (insert execl_last [of "?P @ ?cc2" cfs k'], simp add: execl_all_def,
     auto intro: mpred_merge)
next
  fix b c1 c2 cfs pc s s' stk k
  assume A: "bcomp (b, False, size (ccomp c1) + 1) @ ccomp c1 @
    JMP (size (ccomp c2)) # ccomp c2 ⊨ cfs□"
    (is "?cb @ ?cc1 @ ?i # ?cc2 ⊨ _□")
  let ?P = "?cb @ ?cc1 @ ?i # ?cc2"
  assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc1, s', stk)"
  hence "cfs ! Suc k = (size ?P, s', stk)"
    using A by (insert execl_next [of "?P" cfs k], simp add: execl_all_def,
     drule_tac impI, auto)
  moreover assume "cfs ! 0 = (pc, s, stk)"
  hence "mpred ?P cfs k (Suc k)"
    using C by (simp add: mpred_def msp_def)
  moreover assume "mpred ?P cfs 0 k" 
  ultimately show "mpred ?P cfs 0 (length cfs - Suc 0)"
    using A and B by (insert execl_last [of ?P cfs "Suc k"], simp add: execl_all_def,
     drule_tac impI, auto intro: mpred_merge)
qed

text ‹
\null

Here below are the proofs of theorems @{text m_ccomp_bigstep} and @{text m_ccomp_exec}, which
establish that machine programs simulate source ones and vice versa. The former theorem is inferred
from theorem @{thm [source] ccomp_bigstep} and lemmas @{thm [source] mpred_execl_m_exec},
@{thm [source] ccomp_correct_m}, the latter one from lemma @{thm [source] m_exec_exec} and theorem
@{text ccomp_exec}, in turn derived from lemma @{thm [source] ccomp_correct}.

\null
›

lemma exec_execl [dest!]:
 "P ⊢ cf →* cf' ⟹ ∃cfs. P ⊨ cfs ∧ cfs ≠ [] ∧ hd cfs = cf ∧ last cfs = cf'"
by (erule star.induct, force, erule exE, rule list.exhaust, blast,
 simp del: last.simps, rule exI, subst execl.simps(1), simp)

theorem m_ccomp_bigstep:
 "(c, s) ⇒ s' ⟹
    m_ccomp c ⊢ (0, m_state c s, 0) →* (size (m_ccomp c), m_state c s', 0)"
by (drule ccomp_bigstep [where stk = "[]"], drule exec_execl, clarify,
 frule mpred_execl_m_exec, simp, rule ccomp_correct_m, simp_all add:
 hd_conv_nth last_conv_nth execl_all_def)


theorem ccomp_exec:
 "ccomp c ⊢ (0, s, stk) →* (size (ccomp c), s', stk') ⟹ (c, s) ⇒ s' ∧ stk' = stk"
by (insert ccomp_correct, force simp: hd_conv_nth last_conv_nth execl_all_def cpred_def)

theorem m_ccomp_exec:
 "m_ccomp c ⊢ (0, ms, 0) →* (size (m_ccomp c), ms', sp) ⟹
    (c, state c ms) ⇒ state c ms' ∧ sp = 0"
by (drule m_exec_exec [where stk = "[]"], simp, drule ccomp_exec,
 cases "0 < sp", simp_all, drule add_stack_nnil, blast)

end