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 stk⇩0"}, where @{term stk⇩0} is the initial assembly
stack, that expression gives @{prop "sp' = length stk - length stk⇩0 + length stk' - length stk"},
and the right-hand side matches @{term "length stk' - length stk⇩0"} by library lemma @{thm [source]
add_diff_assoc2} provided that @{prop "length stk⇩0 ≤ 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 stk⇩0"} is not less than the number of the operands taken by @{term P}'s
instruction at offset @{term pc}, and (ii) @{prop "length stk⇩0 ≤ 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 (_, _, stk⇩0) ⇒
  ∀k ∈ {m..<n}. case cfs ! k of (pc, _, stk) ⇒
    msp P pc ≤ length stk - length stk⇩0 ∧ length stk⇩0 ≤ 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 pc⇩0 s⇩0 stk⇩0 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 = (pc⇩0, s⇩0, stk⇩0)" 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 stk⇩0 ∧
      length stk⇩0 ≤ 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 a⇩1 @ acomp a⇩2 @ P ⊨ cfs□;
    ⋀cfs. acomp a⇩1 ⊨ cfs□ ⟹ apred a⇩1 (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. acomp a⇩2 ⊨ cfs□ ⟹ apred a⇩2 (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (∃k < length cfs. cfs ! k =
    (size (acomp a⇩1 @ acomp a⇩2), s, aval a⇩2 s # aval a⇩1 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 a⇩1 s # stk"
 and F' = "λs stk. aval a⇩2 s # stk"], auto simp: apred_def)

lemma bcomp_bcomp:
 "⟦bcomp (b⇩1, f⇩1, i⇩1) @ bcomp (b⇩2, f⇩2, i⇩2) ⊨ cfs□;
    ⋀cfs. bcomp (b⇩1, f⇩1, i⇩1) ⊨ cfs□ ⟹
      bpred (b⇩1, f⇩1, i⇩1) (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. bcomp (b⇩2, f⇩2, i⇩2) ⊨ cfs□ ⟹
      bpred (b⇩2, f⇩2, i⇩2) (cfs ! 0) (cfs ! (length cfs - 1))⟧ ⟹
  case cfs ! 0 of (pc, s, stk) ⇒ pc = 0 ∧ (bval b⇩1 s ≠ f⇩1 ⟶
    (∃k < length cfs. cfs ! k = (size (bcomp (b⇩1, f⇩1, i⇩1) @ bcomp (b⇩2, f⇩2, i⇩2)) +
      (if bval b⇩2 s = f⇩2 then i⇩2 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 b⇩1 s = f⇩1 then i⇩1 else 0"
 and I' = "λs. if bval b⇩2 s = f⇩2 then i⇩2 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 a⇩1 a⇩2 cfs s stk k
  assume A: "acomp a⇩1 @ acomp a⇩2 @ [ADD] ⊨ cfs□"
    (is "?ca⇩1 @ ?ca⇩2 @ ?i ⊨ _□")
  assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca⇩1 + size ?ca⇩2, s, aval a⇩2 s # aval a⇩1 s # stk)"
  hence "cfs ! Suc k = (size (?ca⇩1 @ ?ca⇩2 @ ?i), s, aval (Plus a⇩1 a⇩2) s # stk)"
    using A by (insert execl_next [of "?ca⇩1 @ ?ca⇩2 @ ?i" cfs k],
     simp add: execl_all_def, drule_tac impI, auto)
  thus "apred (Plus a⇩1 a⇩2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    using A and B and C by (insert execl_last [of "?ca⇩1 @ ?ca⇩2 @ ?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 b⇩1 b⇩2 f i cfs s stk
  assume A: "bcomp (b⇩1, False, size (bcomp (b⇩2, f, i)) + (if f then 0 else i)) @
    bcomp (b⇩2, f, i) ⊨ cfs□"
    (is "bcomp (_, _, ?n + ?i) @ ?cb ⊨ _□")
  moreover assume B: "cfs ! 0 = (0, s, stk)" and
   "⋀cb cfs. ⟦cb = ?cb; bcomp (b⇩1, False, ?n + ?i) ⊨ cfs□⟧ ⟹
      bpred (b⇩1, False, ?n + ?i) (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  ultimately have "∃k < length cfs. bpred (b⇩1, False, ?n + ?i)
    (off [] (cfs ! 0)) (off [] (cfs ! k))"
    by (rule_tac execl_all_sub, auto simp: execl_all_def)
  moreover assume C: "¬ bval b⇩1 s"
  ultimately obtain k where D: "k < length cfs" and
    E: "cfs ! k = (size (bcomp (b⇩1, False, ?n + ?i)) + ?n + ?i, s, stk)"
    using B by (auto simp: bpred_def)
  assume "0 ≤ i"
  thus "bpred (And b⇩1 b⇩2, 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 b⇩1 b⇩2 f i cfs s stk k
  assume A: "bcomp (b⇩1, False, size (bcomp (b⇩2, f, i)) + (if f then 0 else i)) @
    bcomp (b⇩2, f, i) ⊨ cfs□"
    (is "?cb⇩1 @ ?cb⇩2 ⊨ _□")
  assume "k < length cfs" and "0 ≤ i" and "bval b⇩1 s" and
   "cfs ! k = (size ?cb⇩1 + size ?cb⇩2 + (if bval b⇩2 s = f then i else 0), s, stk)"
  thus "bpred (And b⇩1 b⇩2, 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 a⇩1 a⇩2 f i cfs s stk k
  assume A: "acomp a⇩1 @ acomp a⇩2 @
    (if f then [JMPLESS i] else [JMPGE i]) ⊨ cfs□"
    (is "?ca⇩1 @ ?ca⇩2 @ ?i ⊨ _□")
  assume B: "k < length cfs" and
    C: "cfs ! k = (size ?ca⇩1 + size ?ca⇩2, s, aval a⇩2 s # aval a⇩1 s # stk)"
  hence D: "cfs ! Suc k =
    (size (?ca⇩1 @ ?ca⇩2 @ ?i) + (if bval (Less a⇩1 a⇩2) s = f then i else 0), s, stk)"
    using A by (insert execl_next [of "?ca⇩1 @ ?ca⇩2 @ ?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 a⇩1 a⇩2, 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 c⇩1 @ ccomp c⇩2 ⊨ cfs□;
    ⋀cfs. ccomp c⇩1 ⊨ cfs□ ⟹ cpred c⇩1 (cfs ! 0) (cfs ! (length cfs - 1));
    ⋀cfs. ccomp c⇩2 ⊨ cfs□ ⟹ cpred c⇩2 (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 c⇩1 @ ccomp c⇩2) ∧
      (c⇩1, s) ⇒ t ∧ (c⇩2, 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'. (c⇩1, s) ⇒ s'" and Q' = "λs s'. (c⇩2, 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 c⇩1 c⇩2 cfs s s' t stk k
  assume "ccomp c⇩1 @ ccomp c⇩2 ⊨ cfs□" and "k < length cfs" and
   "cfs ! k = (size (ccomp c⇩1) + size (ccomp c⇩2), s', stk)"
  moreover assume "(c⇩1, s) ⇒ t" and "(c⇩2, t) ⇒ s'"
  ultimately show "cpred (c⇩1;; c⇩2) (0, s, stk) (cfs ! (length cfs - Suc 0))"
    by (insert execl_last, auto simp: execl_all_def cpred_def)
next
  fix b c⇩1 c⇩2 cfs s stk
  assume A: "bcomp (b, False, size (ccomp c⇩1) + 1) @ ccomp c⇩1 @
    JMP (size (ccomp c⇩2)) # ccomp c⇩2 ⊨ cfs□"
    (is "bcomp ?x @ ?cc⇩1 @ _ # ?cc⇩2 ⊨ _□")
  let ?P = "bcomp ?x @ ?cc⇩1 @ [JMP (size ?cc⇩2)]"
  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. ?cc⇩2 ⊨ cfs□ ⟹ cpred c⇩2 (cfs ! 0) (cfs ! (length cfs - Suc 0))"
  hence "∃k' < length cfs. cpred c⇩2 (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 @ ?cc⇩2) ∧ (c⇩2, s) ⇒ s' ∧ stk' = stk"
    using D by (fastforce simp: cpred_def)
  thus "cpred (IF b THEN c⇩1 ELSE c⇩2) (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 c⇩1 c⇩2 cfs s s' stk k
  assume A: "bcomp (b, False, size (ccomp c⇩1) + 1) @ ccomp c⇩1 @
    JMP (size (ccomp c⇩2)) # ccomp c⇩2 ⊨ cfs□"
    (is "?cb @ ?cc⇩1 @ ?i # ?cc⇩2 ⊨ _□")
  assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc⇩1, s', stk)"
  hence D: "cfs ! Suc k = (size (?cb @ ?cc⇩1 @ ?i # ?cc⇩2), 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 "(c⇩1, s) ⇒ s'"
  thus "cpred (IF b THEN c⇩1 ELSE c⇩2) (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 a⇩1 @ acomp a⇩2 @ P ⊨ cfs□"
      (is "?P ⊨ _□") and
    B: "⋀cfs. acomp a⇩1 ⊨ cfs□ ⟹ mpred (acomp a⇩1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. acomp a⇩2 ⊨ cfs□ ⟹ mpred (acomp a⇩2) cfs 0 (length cfs - 1)"
  shows "case cfs ! 0 of (pc, s, stk) ⇒ ∃k < length cfs.
    cfs ! k = (size (acomp a⇩1 @ acomp a⇩2), s, aval a⇩2 s # aval a⇩1 s # stk) ∧
    mpred ?P cfs 0 k"
proof -
  have "∃k < length cfs. apred a⇩1 (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 a⇩1), s, aval a⇩1 s # stk)"
    using A by (auto simp: apred_def execl_all_def)
  moreover from this have "∃k' < length cfs. apred a⇩2 (off (acomp a⇩1) (cfs ! k))
    (off (acomp a⇩1) (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 a⇩1 @ acomp a⇩2), s, aval a⇩2 s # aval a⇩1 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 (b⇩1, f⇩1, i⇩1) @ bcomp (b⇩2, f⇩2, i⇩2) ⊨ cfs□"
    (is "bcomp ?x⇩1 @ bcomp ?x⇩2 ⊨ _□")
  assumes
    B: "⋀cfs. bcomp ?x⇩1 ⊨ cfs□ ⟹ mpred (bcomp ?x⇩1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. bcomp ?x⇩2 ⊨ cfs□ ⟹ mpred (bcomp ?x⇩2) cfs 0 (length cfs - 1)" and
    D: "size (bcomp ?x⇩2) ≤ i⇩1" and
    E: "0 ≤ i⇩2"
  shows "mpred (bcomp ?x⇩1 @ bcomp ?x⇩2) cfs 0 (length cfs - 1)"
    (is "mpred ?P _ _ _")
proof -
  have "∃k < length cfs. bpred ?x⇩1 (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 ?x⇩1) + (if bval b⇩1 s = f⇩1 then i⇩1 else 0), s, stk)"
    using A by (auto simp: bpred_def execl_all_def)
  moreover from this have "bval b⇩1 s ≠ f⇩1 ⟹ ∃k' < length cfs.
    bpred ?x⇩2 (off (bcomp ?x⇩1) (cfs ! k)) (off (bcomp ?x⇩1) (cfs ! k')) ∧
    mpred (bcomp ?x⇩1 @ bcomp ?x⇩2 @ []) 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 b⇩1 s ≠ f⇩1 ⟹ k' < length cfs ∧ mpred ?P cfs k k' ∧
    fst (cfs ! k') = size ?P + (if bval b⇩2 s = f⇩2 then i⇩2 else 0)"
    using F by (fastforce simp: bpred_def)
  ultimately have "∃k < length cfs. fst (cfs ! k) = (if bval b⇩1 s = f⇩1 then
    size (bcomp ?x⇩1) + i⇩1 else size ?P + (if bval b⇩2 s = f⇩2 then i⇩2 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 a⇩1 a⇩2 cfs pc s stk k
  assume A: "acomp a⇩1 @ acomp a⇩2 @ [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 a⇩1) + size (acomp a⇩2), s,
      aval a⇩2 s # aval a⇩1 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 a⇩1 a⇩2) 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 a⇩1 a⇩2 f i cfs pc s stk k
  assume A: "acomp a⇩1 @ acomp a⇩2 @
    (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 a⇩1) + size (acomp a⇩2), s,
      aval a⇩2 s # aval a⇩1 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 a⇩1 a⇩2) 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 c⇩1 @ ccomp c⇩2 ⊨ cfs□"
      (is "?P ⊨ _□") and
    B: "⋀cfs. ccomp c⇩1 ⊨ cfs□ ⟹ mpred (ccomp c⇩1) cfs 0 (length cfs - 1)" and
    C: "⋀cfs. ccomp c⇩2 ⊨ cfs□ ⟹ mpred (ccomp c⇩2) cfs 0 (length cfs - 1)"
  shows "mpred ?P cfs 0 (length cfs - 1)"
proof -
  have "∃k < length cfs. cpred c⇩1 (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 c⇩1), s', stk)"
    using A by (auto simp: cpred_def execl_all_def)
  moreover from this have "∃k' < length cfs. cpred c⇩2 (off (ccomp c⇩1) (cfs ! k))
    (off (ccomp c⇩1) (cfs ! k')) ∧ mpred (ccomp c⇩1 @ ccomp c⇩2 @ []) 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 c⇩1 c⇩2 cfs pc s s' stk k
  assume A: "bcomp (b, False, size (ccomp c⇩1) + 1) @ ccomp c⇩1 @
    JMP (size (ccomp c⇩2)) # ccomp c⇩2 ⊨ cfs□"
    (is "?cb @ ?cc⇩1 @ ?i # ?cc⇩2 ⊨ _□")
  let ?P = "?cb @ ?cc⇩1 @ [?i]"
  assume B: "cfs ! k = (size ?cb + (size ?cc⇩1 + 1), s', stk)"
  assume "cfs ! 0 = (pc, s, stk)" and "k < length cfs" and
   "⋀cfs. ?cc⇩2 ⊨ cfs□ ⟹ mpred ?cc⇩2 cfs 0 (length cfs - Suc 0)"
  hence "∃k' < length cfs. cpred c⇩2 (off ?P (cfs ! k)) (off ?P (cfs ! k')) ∧
    mpred (?P @ ?cc⇩2 @ []) 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 @ ?cc⇩2) ∧
    mpred (?P @ ?cc⇩2) cfs k k' ∧ k' < length cfs"
    using B by (fastforce simp: cpred_def)
  moreover assume "mpred (?cb @ ?cc⇩1 @ ?i # ?cc⇩2) cfs 0 k"
  ultimately show "mpred (?cb @ ?cc⇩1 @ ?i # ?cc⇩2) cfs 0 (length cfs - Suc 0)"
    using A by (insert execl_last [of "?P @ ?cc⇩2" cfs k'], simp add: execl_all_def,
     auto intro: mpred_merge)
next
  fix b c⇩1 c⇩2 cfs pc s s' stk k
  assume A: "bcomp (b, False, size (ccomp c⇩1) + 1) @ ccomp c⇩1 @
    JMP (size (ccomp c⇩2)) # ccomp c⇩2 ⊨ cfs□"
    (is "?cb @ ?cc⇩1 @ ?i # ?cc⇩2 ⊨ _□")
  let ?P = "?cb @ ?cc⇩1 @ ?i # ?cc⇩2"
  assume B: "k < length cfs" and C: "cfs ! k = (size ?cb + size ?cc⇩1, 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