Theory Turing_HaltingConditions

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

section ‹Halting Conditions and Standard Halting Configuration›

theory Turing_HaltingConditions
  imports Turing_Hoare
begin

subsection ‹Looping of Turing Machines›

definition TMC_loops :: "tprog0 ⇒ nat list ⇒ bool"
  where
    "TMC_loops p ns ≡ (∀stp.¬ is_final (steps0 (1, [], <ns::nat list>) p stp))"

subsection ‹Reaching the Final State›

definition reaches_final :: "tprog0 ⇒ nat list ⇒ bool"
  where
    "reaches_final p ns ≡ ⦃(λtap. tap = ([], <ns>))⦄ p ⦃(λtap. True)⦄"

text ‹The definition @{term reaches_final} and all lemmas about it are only needed for the special halting problem K0. ›

lemma True_holds_for_all: "(λtap. True) holds_for c"
  by (cases c)(auto)

lemma reaches_final_iff: "reaches_final p ns ⟷ (∃n. is_final (steps0 (1, ([], <ns>)) p n))"
  by (auto simp add: reaches_final_def Hoare_halt_def True_holds_for_all)



text ‹Some lemmas about reaching the Final State.›

lemma Hoare_halt_from_init_imp_reaches_final:
  assumes "⦃λtap. tap = ([], <ns>)⦄ p ⦃Q⦄"
  shows "reaches_final p ns"
proof -
  from assms have "∀tap. tap = ([], <ns>) ⟶ (∃n. is_final (steps0 (1, tap) p n))"
    using Hoare_halt_def by auto
  then show ?thesis
    using reaches_final_iff by auto
qed

lemma Hoare_unhalt_impl_not_reaches_final:
  assumes "⦃(λtap. tap = ([], <ns>))⦄ p ↑"
  shows "¬(reaches_final p ns)"
proof 
  assume "reaches_final p ns"
  then have "(∃n. is_final (steps0 (1, ([], <ns>)) p n))" by (auto simp add: reaches_final_iff)
  then obtain n where w_n: "is_final (steps0 (1, ([], <ns>)) p n)" by blast
  from assms have "∀tap. (λtap. tap = ([], <ns>)) tap ⟶ (∀ n . ¬ (is_final (steps0 (1, tap) p n)))"
    by (auto simp add: Hoare_unhalt_def)
  then have "¬ (is_final (steps0 (1, ([], <ns>)) p n))" by blast
  with w_n show False by auto
qed

subsection ‹What is a Standard Tape›

text ‹A tape is called {\em standard}, if the left tape is empty or contains only blanks and
the right tape contains a single nonempty block of strokes (occupied cells) followed by zero or more blanks..

Thus, by definition of left and right tape, the head of the machine is always
scanning the first cell of this single block of strokes.

We extend the notion of a standard tape to lists of numerals as well.
›

definition std_tap :: "tape ⇒ bool"
  where
    "std_tap tap  ≡ (∃k n l. tap = (Bk ↑ k,  <n::nat> @ Bk ↑ l))"

definition std_tap_list :: "tape ⇒ bool"
  where
    "std_tap_list tap  ≡ (∃k ml l. tap = (Bk ↑ k,  <ml::nat list> @ Bk ↑ l))"


lemma "std_tap tap ⟹ std_tap_list tap"
  unfolding std_tap_def std_tap_list_def
  by (metis tape_of_list_def tape_of_nat_list.simps(2))

text ‹A configuration @{term "(st, l, r)"} of a Turing machine is called a {\em standard configuration},
 if the state  @{term "st"} is the final state $0$ and the @{term "(l, r)"} is a standard tape. 
›

(* A duplicate from UTM just for comparison of concepts *)

definition TSTD':: "config ⇒ bool"
  where
    "TSTD' c = ((let (st, l, r) = c in 
             st = 0 ∧ (∃ m. l = Bk↑(m)) ∧ (∃ rs n. r = Oc↑(Suc rs) @ Bk↑(n))))"

(* Relate definition of TSTD' to std_tap *)

lemma "TSTD' (st, l, r) = ((st = 0) ∧ std_tap (l,r))"
  unfolding TSTD'_def std_tap_def
proof -
  have "(let (st, l, r) = (st, l, r) in st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃rs n. r = Oc ↑ Suc rs @ Bk ↑ n))
        = (st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃rs n. r = Oc ↑ Suc rs @ Bk ↑ n))"
    by auto
  also have "... = (st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃n la. r = (<n::nat> @ Bk ↑ la)))"
    by (auto simp add: tape_of_nat_def)
  finally have "(let (st, l, r) = (st, l, r) in st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃rs n. r = Oc ↑ Suc rs @ Bk ↑ n))
                = (st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃n la. r = (<n::nat> @ Bk ↑ la)))"
    by (auto simp add: tape_of_nat_def)
  moreover have "((∃m. l = Bk ↑ m) ∧ (∃n la. r = <n::nat> @ Bk ↑ la)) = (∃k n la. (l, r) = (Bk ↑ k, <n::nat> @ Bk ↑ la))"
    by auto
  ultimately show "(let (st, l, r) = (st, l, r)
                    in  st = 0 ∧ (∃m. l = Bk ↑ m) ∧ (∃rs n. r = Oc ↑ Suc rs @ Bk ↑ n))
                    = 
                    (st = 0 ∧ (∃k n la. (l, r) = (Bk ↑ k, <n::nat> @ Bk ↑ la)))"
    by blast
qed

subsection ‹What does Hoare\_halt mean in general?›

text ‹We say {\em in general} because the result computed on the right tape is not necessarily a numeral but some arbitrary component @{term "r'"} . ›

lemma Hoare_halt2_iff:
"⦃λtap. ∃kl ll. tap = (Bk ↑ kl, r @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄
 ⟷
 (∀kl ll. ∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr)))"
proof
  assume "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, r @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
  then show "∀kl ll. ∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
    using Hoare_halt_E0 is_finalI by force
next
  assume "∀kl ll. ∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
  then show "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, r @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
  unfolding Hoare_halt_def  
  using holds_for.simps by fastforce
qed

lemma Hoare_halt_D:
  assumes "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, r @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
  shows "∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
proof -
  from assms show "∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
    by (simp add: Hoare_halt2_iff is_final_eq)
qed

lemma Hoare_halt_I2:
  assumes "⋀kl ll. ∃n. is_final (steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ kl, r @ Bk ↑ ll)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
  shows "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, r @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
  unfolding Hoare_halt_def  
  using assms holds_for.simps by fastforce


lemma Hoare_halt_D_Nil:
  assumes "⦃λtap. tap = ([], r)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
  shows "∃n. is_final (steps0 (1, ([], r)) p n) ∧ (∃kr lr. steps0 (1, ([], r)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
proof -
  from assms have "⦃λtap. tap = (Bk ↑ 0, r @ Bk ↑ 0)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
    by simp
  then have "∃n. is_final (steps0 (1, (Bk ↑ 0, r @ Bk ↑ 0)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ 0, r @ Bk ↑ 0)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
    using Hoare_halt_E0 append_self_conv assms is_final_eq old.prod.inject prod.inject replicate_0
    by force
  then show ?thesis by auto
qed

lemma Hoare_halt_I2_Nil:
  assumes "∃n. is_final (steps0 (1, ([], r )) p n) ∧ (∃kr lr. steps0 (1, ([], r )) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
  shows "⦃λtap. tap = ([], r)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
proof -
  from assms have "∃n. is_final (steps0 (1, (Bk ↑ 0, r @ Bk ↑ 0)) p n) ∧ (∃kr lr. steps0 (1, (Bk ↑ 0, r @ Bk ↑ 0)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr))"
    by auto
  then have "⦃λtap. tap = (Bk ↑ 0, r @ Bk ↑ 0)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄"
    using Hoare_halt_iff by auto
  then show ?thesis by auto
qed

lemma Hoare_halt2_Nil_iff:
  "⦃λtap. tap = ([], r)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, r' @ Bk ↑ lr)⦄
   ⟷
   (∃n. is_final (steps0 (1, ([], r)) p n) ∧ (∃kr lr. steps0 (1, ([], r)) p n = (0, Bk ↑ kr, r' @ Bk ↑ lr)))"
  using Hoare_halt_D_Nil Hoare_halt_I2_Nil by blast

corollary Hoare_halt_left_tape_Nil_imp_All_left_and_right:
  assumes "⦃λtap.       tap = ([]    , r         )⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k , r' @ Bk ↑ l)⦄"
  shows   "⦃λtap. ∃x y. tap = (Bk ↑ x, r @ Bk ↑ y)⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k , r' @ Bk ↑ l)⦄"
proof -
  from assms have "∃n. is_final (steps0 (1, ([], r)) p n) ∧ (∃k l. steps0 (1, ([], r)) p n = (0, Bk ↑ k,  r' @ Bk ↑ l))"
    using Hoare_halt_D_Nil by auto
  then have "⋀x y. ∃n. is_final (steps0 (1, (Bk ↑ x, r @ Bk ↑ y)) p n) ∧ (∃k l. steps0 (1, (Bk ↑ x, r @ Bk ↑ y)) p n = (0, Bk ↑ k,  r' @ Bk ↑ l))"
    using ex_steps_left_tape_Nil_imp_All_left_and_right
    using is_final.simps by force
  then show ?thesis using Hoare_halt_I2
    by auto
qed

subsubsection ‹What does Hoare\_halt with a numeral list result mean?›

text ‹About computations that result in numeral lists on the final right tape.›

(* Adding trailing blanks to the initial right tape needs tough lemmas (see BlanksDoNotMatter)  *)

lemma TMC_has_num_res_list_without_initial_Bks_imp_TMC_has_num_res_list_after_adding_Bks_to_initial_right_tape:
  " ⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄
  ⟹
    ⦃λtap. ∃ll. tap = ([], <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
proof -
  assume A: "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  then have "∃n. is_final (steps0 (1, ([], <ns::nat list>)) p n) ∧
                 (∃ms kr lr. steps0 (1, ([], <ns::nat list>)) p n = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr))"
    using Hoare_halt_E0 is_finalI by force
  then obtain stp where
    w_stp: "is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧
            (∃ms kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr))"
    by blast

  then obtain ms where  "∃kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)" by blast

  then have "∀ll. ∃kr lr. steps0 (1, ([], <ns::nat list>@ Bk ↑ ll)) p stp = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)"
    using ex_steps_left_tape_Nil_imp_All_left_and_right steps_left_tape_ShrinkBkCtx_to_NIL by blast

  then have "∀ll. is_final (steps0 (1, ([], <ns::nat list>@ Bk ↑ ll)) p stp) ∧
                 (∃ms kr lr. steps0 (1, ([], <ns::nat list>@ Bk ↑ ll)) p stp = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr))"   
    by (metis is_finalI)

  then have "∀tap. (∃ll. tap = ([], <ns::nat list> @ Bk ↑ ll))
                    ⟶ (∃n. is_final (steps0 (1, tap) p n) ∧
                             (λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)) holds_for steps0 (1, tap) p n)"
    using holds_for.simps by force
  then show ?thesis
    unfolding Hoare_halt_def
    by auto
qed

(* Removing trailing blanks on the initial right tape (is easy) *)

lemma TMC_has_num_res_list_without_initial_Bks_iff_TMC_has_num_res_list_after_adding_Bks_to_initial_right_tape:
  "⦃λtap.      tap = ([], <ns::nat list>)          ⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄
    ⟷
   ⦃λtap. ∃ll. tap = ([], <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
proof
  assume "⦃λtap.      tap = ([], <ns::nat list>)          ⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  then show "⦃λtap. ∃ll. tap = ([], <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  using  TMC_has_num_res_list_without_initial_Bks_imp_TMC_has_num_res_list_after_adding_Bks_to_initial_right_tape by blast
next
  assume "⦃λtap. ∃ll. tap = ([], <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  then show "⦃λtap.      tap = ([], <ns::nat list>)          ⦄ p ⦃λtap. ∃ms kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
    by (simp add: Hoare_halt_def assert_imp_def)
qed


(* In addition we may add or remove blanks on the initial left tape *)

lemma TMC_has_num_res_list_without_initial_Bks_imp_TMC_has_num_res_list_after_adding_Bks_to_initial_left_and_right_tape:
  " ⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap.∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄
  ⟹
    ⦃λtap. ∃kl ll. tap = (Bk ↑ kl, <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  using Hoare_halt_left_tape_Nil_imp_All_left_and_right by auto

(*
proof -
  assume A: "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap.∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"

  then have "∃stp. is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧
                   (∃ kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr,  <ms::nat list> @ Bk ↑ lr))"
    using Hoare_halt2_Nil_iff tape_of_list_def tape_of_nat_list.simps(2)  by blast

  then obtain stp where
    w_stp: "is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧
                   (∃ kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr,  <ms::nat list> @ Bk ↑ lr))"
    by blast

  then have "∀kl ll.∃kr lr. steps0 (1, Bk ↑ kl, <ns::nat list> @ Bk ↑ ll) p stp = (0, Bk ↑ kr,  <ms::nat list> @ Bk ↑ lr)"
    using ex_steps_left_tape_Nil_imp_All_left_and_right steps_left_tape_ShrinkBkCtx_to_NIL by blast

  then have "∀kl ll. is_final (steps0 (1, Bk ↑ kl, <ns::nat list> @ Bk ↑ ll) p stp) ∧
                  (∃kr lr. steps0 (1, Bk ↑ kl , <ns::nat list> @ Bk ↑ ll) p stp = (0, Bk ↑ kr,  <ms::nat list> @ Bk ↑ lr))"
    by (metis is_finalI)

  then have "∀tap. (∃kl ll. tap = (Bk ↑ kl, <ns::nat list> @ Bk ↑ ll) )
                    ⟶ (∃stp. is_final (steps0 (1, tap) p stp) ∧
                  (λtap. ∃kr lr. tap = (Bk ↑ kr,  <ms::nat list> @ Bk ↑ lr)) holds_for steps0 (1, tap) p stp)"
    using holds_for.simps by force
  then show ?thesis
    unfolding Hoare_halt_def
    by auto
qed
*)

lemma TMC_has_num_res_list_without_initial_Bks_iff_TMC_has_num_res_list_after_adding_Bks_to_initial_left_and_right_tape:
  " ⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap.∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄
  ⟷
    ⦃λtap. ∃kl ll. tap = (Bk ↑ kl, <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
proof
  assume "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap.∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  then show "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
    using TMC_has_num_res_list_without_initial_Bks_imp_TMC_has_num_res_list_after_adding_Bks_to_initial_left_and_right_tape by auto
next
  assume "⦃λtap. ∃kl ll. tap = (Bk ↑ kl, <ns::nat list> @ Bk ↑ ll)⦄ p ⦃λtap. ∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
  then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap.∃kr lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
    by (simp add: Hoare_halt_def assert_imp_def)
qed


subsection ‹Halting in a Standard Configuration›

subsubsection ‹Definition of Halting in a Standard Configuration›

text ‹The predicates ‹TMC_has_num_res p ns› and ‹TMC_has_num_list_res› describe that
 a run of the Turing program ‹p› on input ‹ns› reaches the final state 0
 and the final tape produced thereby is standard.
 Thus, the computation of the Turing machine ‹p› produced a result, which is
 either a single numeral or a list of numerals.

Since trailing blanks on the initial left or right tape do not matter,
we may restrict our definitions to the case where
 the initial left tape is empty and
 there are no trailing blanks on the initial right tape!
›

definition TMC_has_num_res :: "tprog0 ⇒ nat list ⇒ bool"
  where
    "TMC_has_num_res p ns ≡
     ⦃ λtap. tap = ([], <ns>) ⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"

lemma TMC_has_num_res_iff: "TMC_has_num_res p ns
         ⟷
       (∃stp. is_final (steps0 (1, [],<ns::nat list>) p stp) ∧
              (∃k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)))"
  unfolding TMC_has_num_res_def
proof
  assume "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
  then show "∃stp. is_final (steps0 (1, [], <ns::nat list>) p stp) ∧ (∃k n l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
    by (smt (verit, best) Hoare_halt_E0 Hoare_halt_impl_not_Hoare_unhalt Hoare_unhalt_def is_finalI tape_of_list_def tape_of_nat_def)
next
  assume "∃stp. is_final (steps0 (1, [], <ns::nat list>) p stp) ∧ (∃k n l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
  then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
    by (metis (mono_tags, lifting) Hoare_halt_def holds_for.simps)
qed

(* for clarification
lemma TMC_has_num_res_iff': "TMC_has_num_res p ns ≡
       (∃stp k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
  by (smt TMC_has_num_res_iff is_finalI steps_0 steps_add)
*)

(* --- *)

definition TMC_has_num_list_res :: "tprog0 ⇒ nat list ⇒ bool"
  where
    "TMC_has_num_list_res p ns ≡
     ⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃kr ms lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
 
lemma TMC_has_num_list_res_iff: "TMC_has_num_list_res p ns
         ⟷
       (∃stp. is_final (steps0 (1, [],<ns::nat list>) p stp) ∧
              (∃k ms l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk ↑ l)))"
  unfolding TMC_has_num_list_res_def
proof
  assume "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k ms l. tap = (Bk ↑ k, <ms::nat list> @ Bk ↑ l)⦄"
  then show "∃stp. is_final (steps0 (1, [], <ns::nat list>) p stp) ∧ (∃k ms l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk ↑ l))"
    using Hoare_halt_E0 is_finalI by force
next
  assume "∃stp. is_final (steps0 (1, [], <ns::nat list>) p stp) ∧ (∃k ms l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk ↑ l))"
  then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k ms l.   tap = (Bk ↑ k, <ms::nat list> @ Bk ↑ l)⦄"
    by (metis (mono_tags, lifting) Hoare_halt_def holds_for.simps)
qed

(* for clarification
lemma TMC_has_num_list_res_iff': "TMC_has_num_list_res p ns ≡
        (∃stp k ms l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk ↑ l))"
  by (smt TMC_has_num_list_res_iff is_finalI steps_0 steps_add)
*)

subsubsection ‹Relation between TMC\_has\_num\_res and TMC\_has\_num\_list\_res›

text ‹A computation of a Turing machine, which started on a list of numerals and halts in a
 standard configuration with a single numeral result is a special case of a halt in a standard configuration that
halts with a list of numerals.›

(* FABR: this is an important lemma, since it motivates and validates our extension
 * of various concepts to lists of natural numbers or numerals
 *)

theorem TMC_has_num_res_imp_TMC_has_num_list_res: 
  "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄
   ⟹
   ⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃kr ms lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
proof -
  assume A: "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"

  then have "∃stp. is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧
                 (∃n kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <n::nat> @ Bk ↑ lr))"
    using Hoare_halt_E0 is_finalI by force
  then obtain stp where
    w_stp: "is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧
                 (∃n kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <n::nat> @ Bk ↑ lr))"
    by blast

  then have "(∃n kr lr. steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <n::nat> @ Bk ↑ lr))"
    by auto

  then obtain n kr lr where "steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <n::nat> @ Bk ↑ lr)"
    by blast
  then have "steps0 (1, ([], <ns::nat list>)) p stp = (0, Bk ↑ kr, <[n::nat]> @ Bk ↑ lr)"
    by (simp add: tape_of_list_def)
  then have "is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧ (∃kr lr. (steps0 (1, ([], <ns::nat list>)) p stp) = (0, Bk ↑ kr, <[n::nat]> @ Bk ↑ lr))"
    by (simp add: is_final_eq)

  then have "is_final (steps0 (1, ([], <ns::nat list>)) p stp) ∧ (∃ms kr lr. (steps0 (1, ([], <ns::nat list>)) p stp) = (0, Bk ↑ kr, <ms::nat list> @ Bk ↑ lr))"
    by blast

  then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃kr ms lr. tap = (Bk ↑ kr, <ms::nat list> @ Bk ↑ lr)⦄"
    by (metis (mono_tags, lifting) Hoare_halt_def  holds_for.simps)
qed

corollary TMC_has_num_res_imp_TMC_has_num_list_res': "TMC_has_num_res p ns ⟹ TMC_has_num_list_res p ns"
  unfolding TMC_has_num_res_def TMC_has_num_list_res_def 
  using TMC_has_num_res_imp_TMC_has_num_list_res
  by auto


subsubsection ‹Convenience Lemmas for Halting Problems ›

lemma Hoare_halt_with_Oc_imp_std_tap:
  assumes "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
  shows "TMC_has_num_res p ns"
  unfolding TMC_has_num_res_def
proof -
  from assms have F0: "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄"
    by (auto simp add: tape_of_nat_def)
  show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
    using F0 Hoare_haltI Hoare_halt_E0 Hoare_halt_iff by fastforce
qed

lemma Hoare_halt_with_OcOc_imp_std_tap:
  assumes "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
  shows "TMC_has_num_res p ns"
  unfolding TMC_has_num_res_def
proof -
  from assms have "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄"
    by (auto simp add: tape_of_nat_def)
  then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
    using Hoare_halt_E0 Hoare_halt_iff by fastforce
qed

subsubsection ‹Hoare\_halt on numeral lists with single numeral result›
(* For automation we use Hoare triples directly instead of the concept TMC_has_num_res.
 * Reason: reduce number of theorems used by the simplifier.
 *)

lemma Hoare_halt_on_numeral_imp_result: (* special case of Hoare_halt_D *)
  assumes "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)))⦄"
  shows "∃stp k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk↑ l)"
  using TMC_has_num_res_def TMC_has_num_res_iff assms by blast

lemma Hoare_halt_on_numeral_imp_result_rev: (* special case of Hoare_halt_I2 *)
  assumes "∃stp k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk↑ l)"
  shows "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)))⦄"
  using TMC_has_num_res_def TMC_has_num_res_iff assms is_final_eq by force

lemma Hoare_halt_on_numeral_imp_result_iff: (* special case of Hoare_halt2_iff *)
"⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)))⦄
 ⟷
 (∃stp k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk↑ l))"
  using Hoare_halt_on_numeral_imp_result Hoare_halt_on_numeral_imp_result_rev by blast

subsubsection ‹Hoare\_halt on numeral lists with numeral list result›
(* For automation we use Hoare triples directly instead of the concept TMC_has_num_list_res.
 * Reason: reduce number of theorems used by the simplifier.
 *)

lemma Hoare_halt_on_numeral_imp_list_result: (* special case of Hoare_halt_D *)
  assumes "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k ms l. tap = (Bk ↑ k, <ms::nat list> @ Bk ↑ l)))⦄"
  shows "∃stp k ms l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk↑ l)"  
  using TMC_has_num_list_res_def TMC_has_num_list_res_iff assms by blast

lemma Hoare_halt_on_numeral_imp_list_result_rev: (* special case of Hoare_halt_I2 *)
  assumes "∃stp k ms l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk↑ l)"
  shows "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k ms l. tap = (Bk ↑ k, <ms::nat list> @ Bk ↑ l)))⦄"
  by (metis (mono_tags, lifting) Hoare_haltI assms holds_for.simps is_finalI)

lemma Hoare_halt_on_numeral_imp_list_result_iff: (* special case of Hoare_halt2_iff *)
  "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k ms l. tap = (Bk ↑ k, <ms::nat list> @ Bk ↑ l)))⦄
   ⟷
   (∃stp k ms l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <ms::nat list> @ Bk↑ l))"  
  using Hoare_halt_on_numeral_imp_list_result Hoare_halt_on_numeral_imp_list_result_rev by blast

subsection ‹Trailing left blanks do not matter for computations with result›

(* adding trailing blanks on the initial left tape needs tough lemmas (see BlanksDoNotMatter)  *)

lemma TMC_has_num_res_NIL_impl_TMC_has_num_res_with_left_BKs:
  "⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄
   ⟹
   ⦃(λtap. ∃z. tap = (Bk↑z, <ns>))⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
proof -
  assume   "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
  then have "∃stp k n l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk↑ l)"
    by (rule Hoare_halt_on_numeral_imp_result)

  then obtain n where "∃stp k l. steps0 (1, [],<ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk↑ l)" by blast

  then have "∀z. ∃stp k l. (steps0 (1, (Bk↑z, <ns::nat list>)) p stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
    by (rule ex_steps_left_tape_Nil_imp_All)

  then have "⦃(λtap. ∃z. tap = (Bk↑z, <ns::nat list>))⦄ p ⦃ (λtap. (∃k l. tap = (Bk ↑ k,  <n::nat> @ Bk ↑ l))) ⦄"
    by (rule Hoare_halt_add_Bks_left_tape_L2)
    
  then show "⦃λtap. ∃z. tap = (Bk ↑ z, <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
    using Hoare_halt_iff ‹∀z. ∃stp k l. steps0 (1, Bk ↑ z, <ns>) p stp = (0, Bk ↑ k, <n> @ Bk ↑ l)› by fastforce
qed

(* removing trailing blanks on the initial left tape (is easy) *)

corollary TMC_has_num_res_NIL_iff_TMC_has_num_res_with_left_BKs:
  " ⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄
    ⟷
    ⦃(λtap. ∃z. tap = (Bk↑z, <ns>))⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
proof
  assume "⦃λtap. tap = ([], <ns>)⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
  then show "⦃λtap. ∃z. tap = (Bk ↑ z, <ns>)⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
    using TMC_has_num_res_NIL_impl_TMC_has_num_res_with_left_BKs by blast
next
  assume "⦃λtap. ∃z. tap = (Bk ↑ z, <ns>)⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
  then show "⦃λtap. tap = ([], <ns>)⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
    by (simp add: Hoare_halt_def assert_imp_def)
qed

subsection ‹About Turing Computations and the result they yield›

definition TMC_yields_num_res :: "tprog0 ⇒ nat list ⇒ nat ⇒ bool"
  where "TMC_yields_num_res tm ns n ≡ (∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"

definition TMC_yields_num_list_res :: "tprog0 ⇒ nat list ⇒ nat list ⇒ bool"
  where "TMC_yields_num_list_res tm ns ms ≡ (∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <ms::nat list> @ Bk ↑ l))"

(* This is for documentation and explanation: TMC_yields_num_res_unfolded_into_Hoare_halt *)
lemma TMC_yields_num_res_unfolded_into_Hoare_halt:
  "TMC_yields_num_res tm ns n ≡ ⦃(λtap. tap = ([], <ns>))⦄ tm ⦃(λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk↑ l))⦄"
  by (smt (verit, ccfv_threshold) Hoare_halt_iff TMC_yields_num_res_def)

(* This is for documentation and explanation: TMC_yields_num_list_res_unfolded_into_Hoare_halt *)
lemma TMC_yields_num_list_res_unfolded_into_Hoare_halt:
  "TMC_yields_num_list_res tm ns ms ≡ ⦃(λtap. tap = ([], <ns>))⦄ tm ⦃(λtap. ∃k l. tap = (Bk ↑ k, <ms::nat list> @ Bk↑ l))⦄"
  by (smt (verit, ccfv_threshold) Hoare_halt_E0 Hoare_halt_def Hoare_halt_iff TMC_yields_num_list_res_def)


(* A variant of rule Hoare_plus_halt using TMC_yields_num_list_res and TMC_yields_num_res *)
lemma TMC_yields_num_res_Hoare_plus_halt:
  assumes "TMC_yields_num_list_res tm1 nl r1"
    and "TMC_yields_num_res tm2 r1 r2"
    and "composable_tm0 tm1"
  shows "TMC_yields_num_res (tm1 |+| tm2) nl r2"
proof -
  from assms
  have "⦃λtap. tap = ([], <nl::nat list>)⦄ tm1 ⦃λtap. ∃k l. tap = (Bk ↑ k, <r1::nat list> @ Bk ↑ l)⦄"
    using TMC_yields_num_list_res_unfolded_into_Hoare_halt 
    by auto
  moreover from assms
  have "⦃λtap. tap = ([], <r1>)⦄ tm2 ⦃λtap. ∃k l. tap = (Bk ↑ k, <r2> @ Bk ↑ l)⦄"
    using TMC_yields_num_res_unfolded_into_Hoare_halt
      Hoare_halt_def Hoare_halt_iff TMC_yields_num_res_def by blast
  ultimately
  have "⦃λtap. tap = ([], <nl>)⦄ (tm1 |+| tm2) ⦃λtap. ∃k l. tap = (Bk ↑ k, <r2> @ Bk ↑ l)⦄"  
    using ‹composable_tm0 tm1›
    using Hoare_halt_left_tape_Nil_imp_All_left_and_right Hoare_plus_halt 
    by (simp add: tape_of_list_def)
  then show ?thesis
    using TMC_yields_num_res_unfolded_into_Hoare_halt by auto
qed


(*

 TODO test mixfix notation for TMC_yields_num_res:  ⟪tm: ns ↦ n⟫ 
 TODO test mixfix notation for TMC_has_num_res:     ⟪tm: ns↓⟫ 
 
    Trial for notation of TMC_yields_num_res tm ns n: 
    
      "TMC_yields_num_res tm ns n ≡ (∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
    
         ns ─<tm>→ n
    
         ⟪tm: ns ↝ n⟫   that's good
    
         ⟪tm: ns ↦ n⟫   that's good as well
         
     TMC_has_num_res 
    
      "TMC_has_num_res p ns ≡ ⦃ λtap. tap = ([], <ns>) ⦄ p ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
    
         ⟪tm: ns↓⟫ 

 *)

end