Theory HaltingProblems_K_aux

(* Title: thys/HaltingProblem_K_aux.thy
   Author: Franz Regensburger (FABR) 02/2022
 *)

subsubsection ‹K0: A Variant of the Special Halting Problem K1›

theory HaltingProblems_K_aux
  imports
    HaltingProblems_K_H

begin

(* -------------------------------------------------------------------------- *)

(*
declare adjust.simps[simp del]

declare seq_tm.simps [simp del] 
declare shift.simps[simp del]
declare composable_tm.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]
*)

context hpk
begin

definition K0 :: "(nat list) set"
  where
     "K0 ≡ {nl. (∃n. nl = [n] ∧ reaches_final (c2t n) [n]) }"


text‹Assuming the existence of a Turing Machine K0D0, which is able to decide the set K0,
 we derive a contradiction using the machine @{term "tm_semi_id_gt0"}.
 Thus, we show that the {\em Special Halting Problem K0} is not Turing decidable.
 The proof uses a diagonal argument.
›

lemma existence_of_decider_K0D0_for_K0_imp_False:
  assumes "∃K0D0'. (∀nl.
          (nl ∈ K0 ⟶TMC_yields_num_res K0D0' nl (0::nat))
       ∧  (nl ∉ K0 ⟶TMC_yields_num_res K0D0' nl (1::nat) ))"
  shows False
proof -
  from assms have
    "∃K0D0'. (∀nl.
          (nl ∈ K0 ⟶⦃λtap. tap = ([], <nl>)⦄ K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶⦃λtap. tap = ([], <nl>)⦄ K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄) )"
    unfolding TMC_yields_num_res_unfolded_into_Hoare_halt
    by (simp add: tape_of_nat_def)
  then obtain K0D0' where
    "(∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄) )"
    by blast

(* first, create a composable version of the potentially non-composable machine K0D0' *)

  then have "composable_tm0 (mk_composable0 K0D0') ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ mk_composable0 K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ mk_composable0 K0D0' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄))"
    using Hoare_halt_tm_impl_Hoare_halt_mk_composable0 composable_tm0_mk_composable0 by blast

  then have "∃K0D0. composable_tm0 K0D0 ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄))"
    by blast

  then obtain K0D0 where w_K0D0: "composable_tm0 K0D0 ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄))"
    by blast

  define tm_contra where "tm_contra = K0D0 |+| tm_semi_id_gt0"

(* second, we derive some theorems from our assumptions *)
  have c2t_comp_t2c_TM_eq_for_tm_contra: "c2t (t2c tm_contra) = tm_contra"
    by (auto simp add: c2t_comp_t2c_eq)

(* now, we derive the contradiction *)
  show False 
  proof (cases "[t2c tm_contra] ∈ K0")
    case True
    from ‹[t2c tm_contra] ∈ K0› and w_K0D0 have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
      by auto

    then have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ tm_contra ↑"
      unfolding tm_contra_def

    proof (rule Hoare_plus_unhalt)
      from tm_semi_id_gt0_loops' show "⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄ tm_semi_id_gt0 ↑"
        using Hoare_unhalt_add_Bks_left_tape_L1 Hoare_unhalt_def assms
        by auto
    next
      from w_K0D0 show "composable_tm0 K0D0" by auto
    qed
    then have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ c2t (t2c tm_contra) ↑"
      by (auto simp add: c2t_comp_t2c_TM_eq_for_tm_contra)

    then have "¬(reaches_final (c2t (t2c tm_contra)) [t2c tm_contra])"
      by (simp add: Hoare_unhalt_def Hoare_unhalt_impl_not_reaches_final)

    then have "[t2c tm_contra] ∉ K0"
      by (auto simp add: K0_def)

    with  ‹[t2c tm_contra] ∈ K0› show False by auto
  next  

    case False
    from ‹[t2c tm_contra] ∉ K0› and w_K0D0 have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ K0D0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
      by auto
    then have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ tm_contra ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
      unfolding tm_contra_def

    proof (rule Hoare_plus_halt)
      from tm_semi_id_gt0_halts''
      show "⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄ tm_semi_id_gt0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
        by auto
    next
      from w_K0D0 show "composable_tm0 K0D0" by auto
    qed

    then have
      "⦃λtap. tap = ([], <[t2c tm_contra]>)⦄ c2t (t2c tm_contra) ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
      by (auto simp add: c2t_comp_t2c_TM_eq_for_tm_contra)

    then have
      "reaches_final (c2t (t2c tm_contra)) [t2c tm_contra]"
      by (metis (mono_tags, lifting) Hoare_haltE reaches_final_iff)

    then have "[t2c tm_contra] ∈ K0"
      by (auto simp add: K0_def)

    with ‹[t2c tm_contra] ∉ K0› show False by auto
  qed
qed

text‹Assuming the existence of a Turing Machine K0D1, which is able to decide the set K0,
 we derive a contradiction using the machine @{term "tm_semi_id_eq0"}.
 Thus, we show that the {\em Special Halting Problem K0} is not Turing decidable.
 The proof uses a diagonal argument.
›

lemma existence_of_decider_K0D1_for_K0_imp_False:
  assumes "∃K0D1'. (∀nl.
          (nl ∈ K0 ⟶TMC_yields_num_res K0D1' nl (1::nat))
       ∧  (nl ∉ K0 ⟶TMC_yields_num_res K0D1' nl (0::nat) ))"
  shows False
proof -
  from assms have
    "∃K0D1'. (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄))"
  unfolding TMC_yields_num_res_unfolded_into_Hoare_halt
  by (simp add: tape_of_nat_def)
  then obtain K0D1' where
     "(∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄))"
    by blast

(* first, create a composable version of the potentially non-composable machine K0D1' *)

  then have "composable_tm0 (mk_composable0 K0D1') ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ mk_composable0 K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ mk_composable0 K0D1' ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄))"
    using Hoare_halt_tm_impl_Hoare_halt_mk_composable0 composable_tm0_mk_composable0 by blast

  then have "∃K0D1. composable_tm0 K0D1 ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄))"
    by blast

  then obtain K0D1 where w_K0D1: "composable_tm0 K0D1 ∧ (∀nl.
          (nl ∈ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄)
       ∧  (nl ∉ K0 ⟶ ⦃λtap. tap = ([], <nl>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄))"
    by blast

  define tm_contra where "tm_contra = K0D1 |+| tm_semi_id_eq0"

(* second, we derive some theorems from our assumptions *)
  have c2t_comp_t2c_TM_eq_for_tm_contra: "c2t (t2c tm_contra) = tm_contra"
    by (auto simp add: c2t_comp_t2c_eq)

(* now, we derive the contradiction *)
  show False 
  proof (cases "[t2c tm_contra] ∈ K0")
    case True
    from ‹[t2c tm_contra] ∈ K0› and w_K0D1 have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄"
      by auto

    then have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ tm_contra ↑"
      unfolding tm_contra_def
    proof (rule Hoare_plus_unhalt)
      from tm_semi_id_eq0_loops' show "⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc, Oc] @ Bk ↑ l)⦄ tm_semi_id_eq0 ↑"
        using Hoare_unhalt_add_Bks_left_tape_L1 Hoare_unhalt_def assms
        by auto
    next
      from w_K0D1 show "composable_tm0 K0D1" by auto
    qed

    then have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ c2t (t2c tm_contra) ↑"
      by (auto simp add: c2t_comp_t2c_TM_eq_for_tm_contra)

    then have "¬(reaches_final (c2t (t2c tm_contra)) [t2c tm_contra])"
      by (simp add: Hoare_unhalt_def Hoare_unhalt_impl_not_reaches_final)

    then have "[t2c tm_contra] ∉ K0"
      by (auto simp add: K0_def)

    with  ‹[t2c tm_contra] ∈ K0› show False by auto
  next    
    case False
    from ‹[t2c tm_contra] ∉ K0› and w_K0D1 have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ K0D1 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
      by auto
    then have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ tm_contra ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
      unfolding tm_contra_def
    proof (rule Hoare_plus_halt)
      from tm_semi_id_eq0_halts'' show "⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄ tm_semi_id_eq0 ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
        by auto
    next
      from w_K0D1 show "composable_tm0 K0D1" by auto
    qed

    then have
      "⦃λtap.∃z. tap = ([], <[t2c tm_contra]>)⦄ c2t (t2c tm_contra) ⦃λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑ l)⦄"
      by (auto simp add: c2t_comp_t2c_TM_eq_for_tm_contra)

    then have
      "reaches_final (c2t (t2c tm_contra)) [t2c tm_contra]"
      by (metis (mono_tags, lifting) Hoare_halt_def reaches_final_iff)

    then have "[t2c tm_contra] ∈ K0"
      by (auto simp add: K0_def)

    with ‹[t2c tm_contra] ∉ K0› show False by auto
  qed
qed

corollary not_Turing_decidable_K0: "¬(turing_decidable K0)"
proof
  assume "turing_decidable K0"
  then have "(∃D. (∀nl.
          (nl ∈ K0 ⟶TMC_yields_num_res D nl (1::nat))
       ∧  (nl ∉ K0 ⟶TMC_yields_num_res D nl (0::nat) )))"
    by (auto simp add: turing_decidable_unfolded_into_TMC_yields_conditions tape_of_nat_def)
  with existence_of_decider_K0D1_for_K0_imp_False show False
    by blast
qed


end (* locale hpk *)

end