Theory Turing_Hoare

(* Title: thys/Turing_Hoare.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
 
   Modifications, comments by Franz Regensburger (FABR) 02/2022
 *)

section ‹Hoare Rules for Turing Machines›

theory Turing_Hoare
  imports Numerals
begin


subsection ‹Hoare\_halt and Hoare\_unhalt for total correctness›

subsubsection ‹Definition for Hoare\_halt and Hoare\_unhalt conditions›

type_synonym assert = "tape ⇒ bool"

definition 
  assert_imp :: "assert ⇒ assert ⇒ bool" ("_ ↦ _" [0, 0] 100)
  where
    "P ↦ Q ≡ ∀l r. P (l, r) ⟶ Q (l, r)"

lemma refl_assert[intro, simp]:
  "P ↦ P"
  unfolding assert_imp_def by simp

(* Purpose of the function holds_for:
 * We do not need to apply the selector snd on a configuration c if
 * we just like to apply a predicate to the tape component of the configuration.
 * 
 * We may write 
 *   Q holds_for c
 *  instead of
 *   Q (snd c)
 *)

fun 
  holds_for :: "(tape ⇒ bool) ⇒ config ⇒ bool" ("_ holds'_for _" [100, 99] 100)
  where
    "P holds_for (s, l, r) = P (l, r)"  

lemma is_final_holds[simp]:
  assumes "is_final c"
  shows "Q holds_for (steps c p n) = Q holds_for c"
  using assms 
  by(induct n;cases c,auto)

(* Hoare notation and rules for total correctness *)

(* halting case:
   If the pre-condition P holds for a tape
   then the program p eventually reaches the final state 0 and
   the post-condition holds for (the tape of) the final configuration.
 *)

definition
  Hoare_halt :: "assert ⇒ tprog0 ⇒ assert ⇒ bool" ("(⦃(1_)⦄/ (_)/ ⦃(1_)⦄)" 50)
  where
    "⦃P⦄ p ⦃Q⦄ ≡ (∀tap. P tap ⟶ (∃n. is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n) ))"

(* not halting case:
   If the pre-condition P holds for a tape
   then the program p never reaches the final state 0. 
 *)
definition
  Hoare_unhalt :: "assert ⇒ tprog0 ⇒ bool" ("(⦃(1_)⦄/ (_)) ↑" 50)
  where
    "⦃P⦄ p ↑ ≡ ∀tap. P tap ⟶ (∀ n . ¬(is_final (steps0 (1, tap) p n)))"

lemma Hoare_haltI:
  assumes "⋀l r. P (l, r) ⟹ ∃n. is_final (steps0 (1, (l, r)) p n) ∧ Q holds_for (steps0 (1, (l, r)) p n)"
  shows "⦃P⦄ p ⦃Q⦄"
  unfolding Hoare_halt_def 
  using assms by auto

lemma Hoare_haltE:
  assumes "⦃P⦄ p ⦃Q⦄"
  and "P (l, r)"
shows "∃n. is_final (steps0 (1, (l, r)) p n) ∧ Q holds_for (steps0 (1, (l, r)) p n)"
  using assms by (auto simp add: Hoare_halt_def)

lemma Hoare_unhaltI:
  assumes "⋀l r n. P (l, r) ⟹ ¬ is_final (steps0 (1, (l, r)) p n)"
  shows "⦃P⦄ p ↑"
  unfolding Hoare_unhalt_def 
  using assms 
by auto

lemma Hoare_unhaltE:
  assumes "⦃P⦄ p ↑"
  and  "P tap"
shows "¬ (is_final (steps0 (1, tap) p n))"
proof
  assume major: "is_final (steps0 (1, tap) p n)"
  from assms(1) have "∀tap. P tap ⟶ (∀ n . ¬ (is_final (steps0 (1, tap) p n)))"
    by (auto simp add: Hoare_unhalt_def)
  with assms(2) have "(∀ n . ¬ (is_final (steps0 (1, tap) p n)))" by blast
  with major show "False" by auto
qed

(* Some alternative introduction and elimination rules without intermediate concept holds_for *)
(* Added by FABR *)

lemma Hoare_halt_iff:
 "⦃P⦄ tm ⦃Q⦄
   ⟷ 
  (∀l1 r1. P (l1,r1) ⟶ (∃stp l0 r0.  steps0 (1, l1,r1) tm stp = (0,l0,r0) ∧ Q (l0,r0)))"
  unfolding Hoare_halt_def
proof
  show " ∀tap. P tap ⟶ (∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n)
         ⟹ ∀l1 r1. P (l1, r1) ⟶ (∃stp l0 r0. steps0 (1, l1, r1) tm stp = (0, l0, r0) ∧ Q (l0, r0))"
    by (metis holds_for.elims(2) is_final.simps)
next
  show "∀l1 r1. P (l1, r1) ⟶ (∃stp l0 r0. steps0 (1, l1, r1) tm stp = (0, l0, r0) ∧ Q (l0, r0))
         ⟹ ∀tap. P tap ⟶ (∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n)"
    by (metis before_final holds_for.simps is_finalI old.prod.exhaust)
qed

(* Use like this:

    thm Hoare_halt_iff[THEN iffD1]
    
    ⦃?P1⦄ ?tm1 ⦃?Q1⦄
     ⟹ ∀l1 r1. ?P1 (l1, r1) ⟶ (∃stp l0 r0. steps0 (1, l1, r1) ?tm1 stp = (0, l0, r0) ∧ ?Q1 (l0, r0))
    
    thm Hoare_halt_iff[THEN iffD2]
    
    ∀l1 r1. ?P1 (l1, r1) ⟶ (∃stp l0 r0. steps0 (1, l1, r1) ?tm1 stp = (0, l0, r0) ∧ ?Q1 (l0, r0))
     ⟹ ⦃?P1⦄ ?tm1 ⦃?Q1⦄

 *)

lemma Hoare_halt_I0:
assumes "⋀l1 r1. P(l1, r1) ⟹ steps0 (1, l1, r1) tm stp = (0, l0, r0) ∧ Q (l0, r0)"
shows "⦃P⦄ tm ⦃Q⦄"
  using assms Hoare_halt_iff[THEN iffD2]
  by blast

lemma Hoare_halt_E0:
  assumes major: "⦃P⦄ tm ⦃Q⦄"
and "P(l1, r1)"
shows "∃stp l0 r0. steps0 (1, l1, r1) tm stp = (0, l0, r0) ∧ Q(l0, r0)"
  using assms Hoare_halt_iff[THEN iffD1]
  by (auto simp add: Hoare_halt_def)

(* Despite their triviality, the following lemmas explain our general approach in proving total correctness *)

lemma partial_correctness_and_halts_imp_total_correctness': (* mind the parenthesis arround the premise *)
  assumes partial_corr: "(∃stp l1 r1. P (l1, r1) ∧  is_final (steps0 (1, l1,r1) tm stp)) ⟶ ⦃P⦄ tm ⦃Q⦄"
  and halts: "(∃stp l1 r1. P (l1, r1) ∧  is_final (steps0 (1, l1,r1) tm stp))"
shows "⦃P⦄ tm ⦃Q⦄"
  using halts partial_corr by blast

(* is the same as *)

lemma partial_correctness_and_halts_imp_total_correctness:
  assumes partial_corr: "∀l1 r1 stp. P (l1, r1) ∧ is_final (steps0 (1, l1,r1) tm stp) ⟶ ⦃P⦄ tm ⦃Q⦄"
  and halts: "(∃stp l1 r1. P (l1, r1) ∧  is_final (steps0 (1, l1,r1) tm stp))"
shows "⦃P⦄ tm ⦃Q⦄"
  using halts partial_corr by blast

(* because of simple predicate logic *)

lemma "( (∃stp l1 r1. P (l1, r1) ∧  is_final (steps0 (1, l1,r1) tm stp)) ⟶ ⦃P⦄ tm ⦃Q⦄ )
       ⟷
       (  ∀stp l1 r1. (P (l1, r1) ∧ is_final (steps0 (1, l1,r1) tm stp)  ⟶ ⦃P⦄ tm ⦃Q⦄)  )"
  by blast

(* --- *)

lemma Hoare_consequence:
  assumes "P' ↦ P" "⦃P⦄ p ⦃Q⦄" "Q ↦ Q'"
  shows "⦃P'⦄ p ⦃Q'⦄"
  using assms
  unfolding Hoare_halt_def assert_imp_def
  by (metis holds_for.simps surj_pair)

subsubsection ‹Relation between Hoare\_halt and Hoare\_unhalt›

lemma Hoare_halt_impl_not_Hoare_unhalt:
  assumes "⦃P⦄ p ⦃Q⦄" and "P tap"
  shows "¬(⦃P⦄ p ↑)"
proof
  assume "⦃P⦄ p ↑"
  then have "∀tap. P tap ⟶ (∀ n . ¬ (is_final (steps0 (1, tap) p n)))"
    by (auto simp add: Hoare_unhalt_def)
  with ‹P tap› have L1: "(∀ n . ¬ (is_final (steps0 (1, tap) p n)))" by blast
  from assms have "(∀tap. P tap ⟶ (∃n. is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n) ))"
    by (auto simp add: Hoare_halt_def)
  with ‹P tap› have "(∃n. is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n) )"
    by blast
  then obtain n where w_n: "is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n)" by blast
  then have "is_final (steps0 (1, tap) p n)" by auto
  with L1 show False by auto
qed

lemma Hoare_unhalt_impl_not_Hoare_halt:
  assumes "⦃P⦄ p ↑" and "P tap"
  shows "¬(⦃P⦄ p ⦃Q⦄)"
proof 
  assume "⦃P⦄ p ⦃Q⦄"
  then have
    "(∀tap. P tap ⟶ (∃n. is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n) ))"
    by (auto simp add: Hoare_halt_def)
  with ‹P tap› have "(∃n. is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n) )"
    by blast
  then obtain n where w_n: "is_final (steps0 (1, tap) p n) ∧ Q holds_for (steps0 (1, tap) p n)" by blast
  then have L1: "is_final (steps0 (1, tap) p n)" by auto
  from assms have "∀tap. P tap ⟶ (∀ n . ¬ (is_final (steps0 (1, tap) p n)))"
    by (auto simp add: Hoare_unhalt_def)
  with ‹P tap› have "¬ (is_final (steps0 (1, tap) p n))" by blast
  with L1 show False by auto
qed

subsubsection ‹Hoare\_halt and Hoare\_unhalt for composed Turing Machines›

(*
    Note: "composable_tm (A, 0)" means: A is a composable Turing program

    ⦃P⦄ A ⦃Q⦄   ⦃Q⦄ B ⦃S⦄   (A is composable)
    ----------------------------------------
               ⦃P⦄ A |+| B ⦃S⦄
*)

lemma Hoare_plus_halt [case_names A_halt B_halt A_composable]: 
  assumes A_halt : "⦃P⦄ A ⦃Q⦄"
    and B_halt : "⦃Q⦄ B ⦃S⦄"
    and A_composable : "composable_tm (A, 0)"
  shows "⦃P⦄ A |+| B ⦃S⦄"
proof(rule Hoare_haltI)
  fix l r
  assume h: "P (l, r)"
  then obtain n1 l' r' 
    where "is_final (steps0 (1, l, r) A n1)"  
      and a1: "Q holds_for (steps0 (1, l, r) A n1)"
      and a2: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def
    by (metis is_final_eq surj_pair) 
  then obtain n2 
    where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_composable by (rule_tac seq_tm_next) 
  moreover
  from a1 a2 have "Q (l', r')" by (simp)
  then obtain n3 l'' r''
    where "is_final (steps0 (1, l', r') B n3)" 
      and b1: "S holds_for (steps0 (1, l', r') B n3)"
      and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')"
    using B_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
    using A_composable by (rule_tac seq_tm_final) 
  ultimately show 
    "∃n. is_final (steps0 (1, l, r) (A |+| B) n) ∧ S holds_for (steps0 (1, l, r) (A |+| B) n)"
    using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
qed

(*
    ⦃P⦄ A ⦃Q⦄   ⦃Q⦄ B loops   (A is composable)
    ------------------------------------------
              ⦃P⦄ A |+| B  loops
*)

lemma Hoare_plus_unhalt [case_names A_halt B_unhalt A_composable]:
  assumes A_halt: "⦃P⦄ A ⦃Q⦄"
    and B_uhalt: "⦃Q⦄ B ↑"
    and A_composable : "composable_tm (A, 0)"
  shows "⦃P⦄ (A |+| B) ↑"
proof(rule_tac Hoare_unhaltI)
  fix n l r 
  assume h: "P (l, r)"
  then obtain n1 l' r'
    where a: "is_final (steps0 (1, l, r) A n1)" 
      and b: "Q holds_for (steps0 (1, l, r) A n1)"
      and c: "steps0 (1, l, r) A n1 = (0, l', r')"
    using A_halt unfolding Hoare_halt_def 
    by (metis is_final_eq surj_pair) 
  then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
    using A_composable by (rule_tac seq_tm_next)
  then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
  proof(cases "n2 ≤ n")
    case True
    from b c have "Q (l', r')" by simp
    then have "∀ n. ¬ is_final (steps0 (1, l', r') B n)  "
      using B_uhalt unfolding Hoare_unhalt_def by simp
    then have "¬ is_final (steps0 (1, l', r') B (n - n2))" by auto
    then obtain s'' l'' r'' 
      where "steps0 (1, l', r') B (n - n2) = (s'', l'', r'')" 
        and "¬ is_final (s'', l'', r'')" by (metis surj_pair)
    then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
      using A_composable by (auto dest: seq_tm_second simp del: composable_tm.simps)
    then have "¬ is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
      using A_composable by (simp only: steps_add eq) simp
    then show "¬ is_final (steps0 (1, l, r) (A |+| B) n)" 
      using ‹n2 ≤ n› by simp
  next 
    case False
    then obtain n3 where "n = n2 - n3"
      using diff_le_self le_imp_diff_is_add nat_le_linear
        add.commute by metis
    moreover
    with eq show "¬ is_final (steps0 (1, l, r) (A |+| B) n)"
      by (simp add: not_is_final[where ?n1.0="n2"])
  qed
qed

subsection ‹Trailing Blanks on the left tape do not matter for Hoare\_halt›

text ‹The following theorems have major impact on the definition of Turing Computability.›

lemma Hoare_halt_add_Bks_left_tape_L1:
  assumes "⦃ λtap. tap = ([], r)⦄ p ⦃ (λtap. ∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l)) ⦄"
  shows   "∀z. ∃stp k l. (steps0 (1, Bk↑z,r) p stp) = (0, Bk ↑ k, CR @ Bk ↑ l)"
proof -
  from assms
  have "∃stp. is_final (steps0 (1, [], r) p stp) ∧ (λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, [], r) p stp"
    using Hoare_haltE[OF assms] by auto
  then obtain stp where
    w: "is_final (steps0 (1, [], r) p stp) ∧ (λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, [], r) p stp" by blast
  then have  "∃k  l. snd(steps0 (1, [], r) p stp) = (Bk ↑ k, CR @ Bk ↑ l)"
  proof (cases " steps0 (1, [], r) p stp")
    case (fields s' l' r')
    then have "steps0 (1, [], r) p stp = (s', l', r')" .
    then show ?thesis
      using w holds_for.simps snd_conv by auto
  qed
  moreover from w have "fst (steps0 (1, [], r) p stp) = 0"
    by (metis is_final_eq surjective_pairing)
  ultimately have "∃stp k l. steps0 (1, [], r) p stp = (0, Bk ↑ k, CR @ Bk ↑ l)"
    by (metis surjective_pairing)
  then have "∀z. ∃stp k l. (steps0 (1, (Bk↑z, r)) p stp) = (0, Bk ↑ k, CR @ Bk ↑ l)"
    using steps_left_tape_Nil_imp_All 
    by blast
  then show ?thesis
    by blast
qed

lemma Hoare_halt_add_Bks_left_tape_L2:
  assumes "∀z. ∃stp k l. (steps0 (1, Bk↑z,r) p stp) = (0, Bk ↑ k, CR @ Bk ↑ l)"
  shows "⦃(λtap. ∃z. tap = (Bk↑z, r))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l))) ⦄"
  unfolding Hoare_halt_def
proof 
  fix tap
  show "(∃z. tap = (Bk ↑ z, r)) ⟶ (∃n. is_final (steps0 (1, tap) p n) ∧
                                   (λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, tap) p n)"
  proof
    assume A: "∃z. tap = (Bk ↑ z, r)"
    from assms have B: "⋀z. ∃stp k l. steps0 (1, Bk ↑ z, r) p stp = (0, Bk ↑ k, CR @ Bk ↑ l)" by blast
    from A obtain z2 where w_z: "tap = (Bk ↑ z2, r)" by blast
    from B obtain stp k l where w: "(steps0 (1, (Bk↑z2, r)) p stp) = (0, Bk ↑ k, CR @ Bk ↑ l)"
      by blast

    show "∃n. is_final (steps0 (1, tap) p n) ∧ (λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, tap) p n"
    proof
      show "is_final (steps0 (1, tap) p stp) ∧ (λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, tap) p stp"
      proof
        from w and w_z       
        show "is_final (steps0 (1, tap) p stp)" by (auto simp add: is_final_eq)
      next
        from w and w_z show "(λtap. ∃k l. tap = (Bk ↑ k, CR @ Bk ↑ l)) holds_for steps0 (1, tap) p stp"
          by auto
      qed
    qed
  qed
qed

theorem Hoare_halt_add_Bks_left_tape:
  "⦃(λtap.     tap = ([]  , r))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l))) ⦄
  ⟹
   ∀z.  ⦃(λtap. tap = (Bk↑z, r))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l))) ⦄"
  using Hoare_halt_add_Bks_left_tape_L1 Hoare_halt_add_Bks_left_tape_L2
  by (simp add: Hoare_haltI  Hoare_halt_def Pair_inject old.prod.exhaust )

theorem Hoare_halt_del_Bks_left_tape:
  "⦃(λtap. ∃z. tap = (Bk↑z, r))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l))) ⦄
  ⟹
   ⦃(λtap.     tap = ([]  , r))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  CR @ Bk ↑ l))) ⦄"
  unfolding Hoare_halt_def
  by auto

(* Hoare unhalt *)

lemma is_final_del_Bks: "is_final (steps0 (s, Bk ↑ k, r) tm stp) ⟹ is_final (steps0 (s, [], r) tm stp)"
proof (cases k)
  assume "is_final (steps0 (s, Bk ↑ k, r) tm stp)"
    and "k=0"
  case 0
  then show ?thesis
    using ‹is_final (steps0 (s, Bk ↑ k, r) tm stp)› replicate_0 by auto
next
  fix nat
  assume A: "is_final (steps0 (s, Bk ↑ k, r) tm stp)" and "k = Suc nat"
  then have B: "0 <k" by auto
  have "∃ l' r'. (steps0 (s, Bk ↑ k, r) tm stp) = (0, l', r')"
  proof (cases "steps0 (s, Bk ↑ k, r) tm stp")
    case (fields a b c)
    then show ?thesis
      using A is_final_eq by auto
  qed
  then obtain l' r' where w: "steps0 (s, Bk ↑ k, r) tm stp = (0, l', r')" by blast
  then have "steps0 (s, []@Bk ↑ k, r) tm stp = (0, l', r')" by auto

  with B have "∃zb CL'. l' = CL'@Bk↑zb  ∧ steps0 (s,[], r) tm stp = (0,CL',r')"
    using steps_left_tape_ShrinkBkCtx_arbitrary_CL
    by auto
  then obtain zb CL' where "l' = CL'@Bk↑zb  ∧ steps0 (s,[], r) tm stp = (0,CL',r')" by blast
  then show ?thesis by auto
qed

lemma Hoare_unhalt_add_Bks_left_tape_L1:
  assumes "⦃λtap. tap = ([], r)⦄ p ↑"
  shows "∀z. ⦃λtap. tap = (Bk ↑ z, r)⦄ p ↑"
proof -
  from assms have "⋀stp. ¬ is_final (steps0 (1, [], r) p stp)"
    using Hoare_unhaltE[OF assms] by auto
  then have "⋀stp z. ¬ is_final (steps0 (1, Bk ↑ z, r) p stp)"
    using is_final_del_Bks
    by blast
  then show ?thesis
    by (simp add: Hoare_unhaltI Hoare_unhalt_def)
qed

subsection ‹Halt lemmas with respect to function mk\_composable0›

theorem Hoare_halt_tm_impl_Hoare_halt_mk_composable0_cell_list: "⦃λtap. tap = ([], cl)⦄ tm ⦃Q⦄ ⟹ ⦃λtap. tap = ([], cl)⦄ mk_composable0 tm ⦃Q⦄" 
  unfolding Hoare_halt_def
proof -
  assume A: "∀tap. (tap = ([], cl)) ⟶ (∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n)"
  show "∀tap. (tap = ([], cl)) ⟶ (∃n. is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n)"
  proof
    fix tap
    show "(tap = ([], cl)) ⟶ (∃n. is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n)"
    proof
      assume "tap = ([], cl)"
      with A have "(∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n)"
        by auto
      then obtain n where w_n: "is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n"
        by blast

      with ‹tap = ([], cl)› have w_n': "is_final (steps0 (1, [], cl) tm n) ∧ Q holds_for steps0 (1, [], cl) tm n" by auto

      have "∃n. is_final (steps0 (1, [], cl) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) n"

      proof (cases "∀stp. steps0 (1,[],cl) (mk_composable0 tm) stp = steps0 (1,[], cl) tm stp")
        case True
        with w_n' have "is_final (steps0 (1, [], cl) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) n" by auto
        then show ?thesis by auto
      next
        case False
        then have "∃stp. steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast
        then obtain stp where w_stp: "steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast

        show "∃m. is_final (steps0 (1, [], cl) (mk_composable0 tm) m) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) m"
        proof -
          from w_stp have F0: "0 < stp ∧
                           (∃fl fr.
                                   snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr)))"
            by (rule mk_composable0_tm_at_most_one_diff')

          from F0 have "0 < stp" by auto

          from F0 obtain fl fr where w_fl_fr: "snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr))" by blast


          have "steps0 (1, [], cl) tm (stp+1) = steps0 (1, [], cl) tm  n"
          proof (cases "steps0 (1, [], cl) tm n")
            case (fields fsn fln frn)
            then have "steps0 (1, [], cl) tm n = (fsn, fln, frn)" .
            with w_n' have "is_final (fsn, fln, frn)" by auto
            with is_final_eq have "fsn=0" by auto
            with ‹steps0 (1, [], cl) tm n = (fsn, fln, frn)›  have "steps0 (1, [], cl) tm n = (0, fln, frn)" by auto

            show "steps0 (1, [], cl) tm (stp + 1) = steps0 (1, [], cl) tm n"
            proof (cases "n ≤ stp+1")
              case True
              then have "n ≤ stp + 1" .
              show ?thesis
              proof -
                from ‹steps0 (1, [], cl) tm n = (0, fln, frn)› and ‹n ≤ stp + 1› have "steps0 (1, [], cl) tm (stp+1) = (0, fln, frn)"
                  by (rule stable_config_after_final_ge_2')
                with ‹fsn=0› and ‹steps0 (1, [], cl) tm n = (fsn, fln, frn)› show ?thesis by auto
              qed
            next
              case False
              then have "stp + 1 ≤ n" by arith
              show ?thesis
              proof -
                from w_fl_fr have "steps0 (1, [], cl) tm (stp+1) = (0, fl, fr)" by auto
                have "steps0 (1, [], cl) tm n = (0, fl, fr)"
                proof (rule stable_config_after_final_ge_2')
                  from ‹steps0 (1, [], cl) tm (stp+1) = (0, fl, fr)› show "steps0 (1, [], cl) tm (stp+1) = (0, fl, fr)" by auto
                next
                  from ‹stp + 1 ≤ n› show "stp + 1 ≤ n" .
                qed
                with ‹steps0 (1, [], cl) tm (stp+1) = (0, fl, fr)› show ?thesis by auto
              qed
            qed
          qed

          with w_n' have "is_final(steps0 (1, [], cl) tm (stp+1)) ∧ Q holds_for steps0 (1, [], cl) tm (stp+1)" by auto
          moreover from w_fl_fr have "steps0 (1, [], cl) tm (stp+1) = steps0 (1, [], cl) (mk_composable0 tm) (stp+1)" by auto
          ultimately have "is_final(steps0 (1, [], cl) (mk_composable0 tm) (stp+1)) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) (stp+1)" by auto
          then show ?thesis by blast
        qed
      qed
      with ‹tap = ([], cl)› show "∃n. is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n" by auto
    qed
  qed
qed

theorem Hoare_halt_tm_impl_Hoare_halt_mk_composable0_cell_list_rev: "⦃λtap. tap = ([], cl)⦄ mk_composable0 tm ⦃Q⦄ ⟹ ⦃λtap. tap = ([], cl)⦄ tm ⦃Q⦄" 
  unfolding Hoare_halt_def
proof -
  assume A: "∀tap. tap = ([], cl) ⟶ (∃n. is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n)"
  show "∀tap. tap = ([], cl) ⟶ (∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n)"
  proof
    fix tap
    show "(tap = ([], cl) ⟶ (∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n))"
    proof
      assume "tap = ([], cl)"
      with A have "(∃n. is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n)"
        by auto
      then obtain n where w_n: "is_final (steps0 (1, tap) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, tap) (mk_composable0 tm) n"
        by blast

      with ‹tap = ([], cl)› have w_n': "is_final (steps0 (1, [], cl) (mk_composable0 tm) n) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) n" by auto

      have "∃n. is_final (steps0 (1, [], cl) tm n) ∧ Q holds_for steps0 (1, [], cl) tm n"

      proof (cases "∀stp. steps0 (1,[],cl) (mk_composable0 tm) stp = steps0 (1,[], cl) tm stp")
        case True
        with w_n' have "is_final (steps0 (1, [], cl)  tm n) ∧ Q holds_for steps0 (1, [], cl)  tm n" by auto
        then show ?thesis by auto
      next
        case False
        then have "∃stp. steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast
        then obtain stp where w_stp: "steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast

        show "∃m. is_final (steps0 (1, [], cl) tm m) ∧ Q holds_for steps0 (1, [], cl) tm m"
        proof -
          from w_stp have F0: "0 < stp ∧
                           (∃fl fr.
                                   snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr)))"
            by (rule mk_composable0_tm_at_most_one_diff')

          from F0 have "0 < stp" by auto

          from F0 obtain fl fr where w_fl_fr: "snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr))" by blast


          have "steps0 (1, [], cl) (mk_composable0 tm) (stp+1) = steps0 (1, [], cl) (mk_composable0 tm)  n"
            by (metis One_nat_def add_Suc_right is_final.elims(2) less_add_one nat_le_linear stable_config_after_final_ge w_fl_fr w_n')
          with w_n' have "is_final(steps0 (1, [], cl) (mk_composable0 tm) (stp+1)) ∧ Q holds_for steps0 (1, [], cl) (mk_composable0 tm) (stp+1)" by auto
          moreover from w_fl_fr have "steps0 (1, [], cl) tm (stp+1) = steps0 (1, [], cl) (mk_composable0 tm) (stp+1)" by auto
          ultimately have "is_final(steps0 (1, [], cl)  tm (stp+1)) ∧ Q holds_for steps0 (1, [], cl) tm (stp+1)" by auto
          then show ?thesis by blast
        qed
      qed
      with ‹tap = ([], cl)› show "∃n. is_final (steps0 (1, tap) tm n) ∧ Q holds_for steps0 (1, tap) tm n" by auto
    qed
  qed
qed

lemma Hoare_unhalt_tm_impl_Hoare_unhalt_mk_composable0_cell_list: "(⦃λtap. tap = ([], cl )⦄ tm ↑) ⟹ (⦃λtap. tap = ([], cl) ⦄ (mk_composable0 tm) ↑)" 
  unfolding Hoare_unhalt_def
proof -
  assume A: " ∀tap. (tap = ([], cl)) ⟶ (∀n. ¬ is_final (steps0 (1, tap) tm n))"
  show  "∀tap. (tap = ([], cl)) ⟶ (∀n. ¬ is_final (steps0 (1, tap) (mk_composable0 tm) n))"
  proof
    fix tap
    show "(tap = ([], cl)) ⟶ (∀n. ¬ is_final (steps0 (1, tap) (mk_composable0 tm) n))"
    proof
      assume "tap = ([], cl)"
      with A have B: "∀n. ¬ is_final (steps0 (1, tap) tm n)" by auto

      show "∀n. ¬ is_final (steps0 (1, tap) (mk_composable0 tm) n)"
      proof (cases "∀stp. steps0 (1,[], cl) (mk_composable0 tm) stp = steps0 (1,[], cl) tm stp")
        case True
        then have "∀stp. steps0 (1, [], cl) (mk_composable0 tm) stp = steps0 (1, [], cl) tm stp" .
        show ?thesis
        proof
          fix n

          from ‹∀stp. steps0 (1, [], cl) (mk_composable0 tm) stp = steps0 (1, [], cl) tm stp›
          have "steps0 (1, [], cl) (mk_composable0 tm) n = steps0 (1, [], cl) tm n" by auto
          moreover from B and ‹tap = ([], cl)› have "¬ is_final (steps0 (1, [], cl) tm n)" by auto
          ultimately have "¬ is_final (steps0 (1, [], cl)  (mk_composable0 tm) n)" by auto
          with  ‹tap = ([], cl)› show "¬ is_final (steps0 (1, tap)  (mk_composable0 tm) n)" by auto
        qed
      next
        case False
        then have "¬ (∀stp. steps0 (1, [], cl) (mk_composable0 tm) stp = steps0 (1, [], cl) tm stp)" .
        then have "∃stp. steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast
        then obtain stp where w_stp: "steps0 (1, [], cl) (mk_composable0 tm) stp ≠ steps0 (1, [], cl) tm stp" by blast

        show "∀n. ¬ is_final (steps0 (1, tap) (mk_composable0 tm) n)"
        proof -
          from w_stp have F0: "0 < stp ∧
                           (∃fl fr.
                                   snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr)))"
            by (rule mk_composable0_tm_at_most_one_diff')
          then have "(∃fl fr.
                                   snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr)))" by auto
          then obtain fl fr where w_fl_fr: "snd (steps0 (1, [], cl) tm stp) = (fl, fr) ∧
                                   (∀i < stp. steps0 (1, [], cl) (mk_composable0 tm) i = steps0 (1, [], cl) tm i) ∧
                                   (∀j > stp. steps0 (1, [], cl) tm (j) = (0, fl, fr) ∧ 
                                              steps0 (1, [], cl) (mk_composable0 tm) j =(0, fl, fr))" by blast
          then have "steps0 (1, [], cl) tm (stp+1) = (0, fl, fr)" by auto
          then have "is_final (steps0 (1, [], cl) tm (stp+1))" by auto
          with ‹tap = ([], cl)› have "is_final (steps0 (1, tap) tm (stp+1))" by auto
          moreover from B have "¬ is_final (steps0 (1, tap) tm (stp+1))" by blast
          ultimately have False by auto
          then show ?thesis by auto
        qed
      qed
    qed
  qed
qed

(* --- trivial specializations for cells generated from lists of natural numbers or pairs of such cell lists --- *)

corollary Hoare_halt_tm_impl_Hoare_halt_mk_composable0: "⦃λtap. tap = ([]::cell list, <nl>)⦄ tm ⦃Q⦄ ⟹ ⦃λtap. tap = ([], <nl>)⦄ mk_composable0 tm ⦃Q⦄"
  using Hoare_halt_tm_impl_Hoare_halt_mk_composable0_cell_list by auto

corollary Hoare_unhalt_tm_impl_Hoare_unhalt_mk_composable0: "(⦃λtap. tap = ([], <nl>)⦄ tm ↑) ⟹ (⦃λtap. tap = ([], <nl>)⦄ (mk_composable0 tm) ↑)"
  using Hoare_unhalt_tm_impl_Hoare_unhalt_mk_composable0_cell_list by auto

(* --- *)

corollary Hoare_halt_tm_impl_Hoare_halt_mk_composable0_pair:
  "⦃λtap. tap = ([], <(nl1,nl2)>)⦄ tm ⦃Q⦄ ⟹ ⦃λtap. tap = ([], <(nl1,nl2)>)⦄ mk_composable0 tm ⦃Q⦄"
  using Hoare_halt_tm_impl_Hoare_halt_mk_composable0_cell_list by auto

corollary Hoare_unhalt_tm_impl_Hoare_unhalt_mk_composable0_pair: "(⦃λtap. tap = ([], <(nl1, nl2)>)⦄ tm ↑) ⟹ (⦃λtap. tap = ([], <(nl1,nl2)>)⦄ (mk_composable0 tm) ↑)"
  using Hoare_unhalt_tm_impl_Hoare_unhalt_mk_composable0_cell_list by auto


section ‹The Halt Lemma: no infinite descend›

lemma halt_lemma: 
  "⟦wf LE; ∀n. (¬ P (f n) ⟶ (f (Suc n), (f n)) ∈ LE)⟧ ⟹ ∃n. P (f n)"
  by (metis wf_iff_no_infinite_down_chain)

end