Theory TuringUnComputable_H2_original

(* Title: thys/TuringUnComputable_H2_original.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten

   Further contributions by Franz Regensburger (FABR) 02/2022:
   * Re-ordering of sections
   * Added comments

   Editorial note FABR:
   this file was part of the theory file Uncomputable.thy
   in the original AFP entry. 
   
 *)

subsubsection ‹Undecidability of the General Halting Problem H, Variant 2, original version›

theory TuringUnComputable_H2_original
  imports
    DitherTM
    CopyTM

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]
*)

(* Cleanup the global simpset for proofs of several theorems about tm_dither *)

(*
declare adjust.simps[simp del]
*)

text ‹The diagonal argument below shows the undecidability of a variant of the
 General Halting Problem. Implicitly, we thus show that the General Halting Function
 (the characteristic function of the Halting Problem) is not Turing computable.›

(*

Turing_HaltingConditions.thy:

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)) ⦄"

DitherTM.thy:

lemma composable_tm0_tm_dither[intro, simp]: "composable_tm0 tm_dither"
  by (auto simp: composable_tm.simps tm_dither_def)

CopyTM.thy:

lemma composable_tm0_tm_copy[intro, simp]: "composable_tm0 tm_copy"
  by (auto simp: tm_copy_def)

*)

text ‹
  The following locale specifies that some TM ‹H› can be used to decide 
  the {\em General Halting Problem} and ‹False› is going to be derived 
  under this locale. Therefore, the undecidability of the  {\em  General Halting Problem}
  is established.

  The proof makes use of the TMs ‹tm_copy› and ‹tm_dither›.
›

locale uncomputable = 
  (* Interestingly, the detailed definition of the coding function @{text "code"} for Turing machines
     does not affect the final result. In the proof there is no need to appeal on properties of the coding function
     like e.g. injectivity! *)

fixes code :: "instr list ⇒ nat" 
  (* 
   * The TM "H" is the one which is assumed being able to solve the general Halting problem.
   *)
  and H :: "instr list"

  (* FABR Note:
   * The next axiom states that the Turing machine H is well-formed (composable).
   * However, this manifests a bug in the modelling of this locale!
   *
   * Due to this local axiom, we only prove that there exists no composable TM H
   * that is able to decide the Halting problem 'TMC_has_num_res M ns'
   *
   * See theories composableTMs and HaltingProblem_K for a fix by FABR.
   *
   *)

assumes h_composable[intro]: "composable_tm0 H"


  (*
   * The following two local axioms specify (claim) that the Turing Machine H
   * is able to decide the general Halting problem H2.
   *)

and h_case:
"⋀ M ns.  TMC_has_num_res M ns ⟹ ⦃(λtap. tap = ([Bk], <(code M, ns)>))⦄ H ⦃(λtap. ∃k. tap = (Bk ↑ k, <0::nat>))⦄"
and nh_case: 
"⋀ M ns. ¬  TMC_has_num_res M ns ⟹ ⦃(λtap. tap = ([Bk], <(code M, ns)>))⦄ H ⦃(λtap. ∃k. tap = (Bk ↑ k, <1::nat>))⦄"
begin

(* Assertions for the Turing Machine H *)
abbreviation (input)
  "pre_H_ass M ns ≡ λtap. tap = ([Bk], <(code M, ns::nat list)>)"

abbreviation (input)
  "post_H_halt_ass ≡ λtap. ∃k. tap = (Bk ↑ k, <1::nat>)"

abbreviation (input)
  "post_H_unhalt_ass ≡ λtap. ∃k. tap = (Bk ↑ k, <0::nat>)"


lemma H_halt:
  assumes "¬  TMC_has_num_res M ns" 
  shows "⦃pre_H_ass M ns⦄ H ⦃post_H_halt_ass⦄"
  using assms nh_case by auto

lemma H_unhalt:
  assumes " TMC_has_num_res M ns" 
  shows "⦃pre_H_ass M ns⦄ H ⦃post_H_unhalt_ass⦄"
  using assms h_case by auto

(* The TM tcontra is the culprit that is used to derive a contradiction *)

definition
  "tcontra ≡ (tm_copy |+| H) |+| tm_dither"
abbreviation
  "code_tcontra ≡ code tcontra"

(* assume tcontra does not halt on its code *)
lemma tcontra_unhalt: 
  assumes "¬  TMC_has_num_res tcontra [code tcontra]"
  shows "False"
proof -
  (* invariants *)
  define P1 where "P1 ≡ λtap. tap = ([]::cell list, <code_tcontra>)"
  define P2 where "P2 ≡ λtap. tap = ([Bk], <(code_tcontra, code_tcontra)>)"
  define P3 where "P3 ≡ λtap. ∃k. tap = (Bk ↑ k, <1::nat>)"

(*
  ⦃P1⦄ tm_copy ⦃P2⦄  ⦃P2⦄ H ⦃P3⦄ 
  ----------------------------
     ⦃P1⦄ (tm_copy |+| H) ⦃P3⦄     ⦃P3⦄ tm_dither ⦃P3⦄
  ------------------------------------------------
                 ⦃P1⦄ tcontra ⦃P3⦄
  *)

  have H_composable: "composable_tm0 (tm_copy |+| H)" by auto

(* ⦃P1⦄ (tm_copy |+| H) ⦃P3⦄ *)
  have first: "⦃P1⦄ (tm_copy |+| H) ⦃P3⦄" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tm_copy *)
    show "⦃P1⦄ tm_copy ⦃P2⦄" unfolding P1_def P2_def tape_of_nat_def
      by (rule tm_copy_correct)
  next
    case B_halt (* of H *)
    show "⦃P2⦄ H ⦃P3⦄"
      unfolding P2_def P3_def 
      using H_halt[OF assms]
      by (simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* ⦃P3⦄ tm_dither ⦃P3⦄ *)
  have second: "⦃P3⦄ tm_dither ⦃P3⦄" unfolding P3_def 
    by (rule tm_dither_halts)

(* ⦃P1⦄ tcontra ⦃P3⦄ *)
  have "⦃P1⦄ tcontra ⦃P3⦄" 
    unfolding tcontra_def
    by (rule Hoare_plus_halt[OF first second H_composable])

  with assms show "False"
    unfolding P1_def P3_def
    unfolding  TMC_has_num_res_def
    unfolding Hoare_halt_def 
    apply(auto) apply(rename_tac n)
    apply(drule_tac x = n in spec)
    apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
    apply(auto simp add: tape_of_list_def)
    by (metis append_Nil2 replicate_0)
qed

(* asumme tcontra halts on its code *)
lemma tcontra_halt: 
  assumes " TMC_has_num_res tcontra [code tcontra]"
  shows "False"
proof - 
  (* invariants *)
  define P1 where "P1 ≡ λtap. tap = ([]::cell list, <code_tcontra>)"
  define P2 where "P2 ≡ λtap. tap = ([Bk], <(code_tcontra, code_tcontra)>)"
  define Q3 where "Q3 ≡ λtap. ∃k. tap = (Bk ↑ k, <0::nat>)"

(*
  ⦃P1⦄ tm_copy ⦃P2⦄  ⦃P2⦄ H ⦃Q3⦄ 
  ----------------------------
     ⦃P1⦄ (tm_copy |+| H) ⦃Q3⦄     ⦃Q3⦄ tm_dither loops
  ------------------------------------------------
               ⦃P1⦄ tcontra loops
  *)

  have H_composable: "composable_tm0 (tm_copy |+| H)" by auto

(* ⦃P1⦄ (tm_copy |+| H) ⦃Q3⦄ *)
  have first: "⦃P1⦄ (tm_copy |+| H) ⦃Q3⦄" 
  proof (cases rule: Hoare_plus_halt)
    case A_halt (* of tm_copy *)
    show "⦃P1⦄ tm_copy ⦃P2⦄" unfolding P1_def P2_def tape_of_nat_def
      by (rule tm_copy_correct)
  next
    case B_halt (* of H *)
    then show "⦃P2⦄ H ⦃Q3⦄"
      unfolding P2_def Q3_def using H_unhalt[OF assms]
      by(simp add: tape_of_prod_def tape_of_list_def)
  qed (simp)

(* ⦃P3⦄ tm_dither loops *)
  have second: "⦃Q3⦄ tm_dither ↑" unfolding Q3_def 
    by (rule tm_dither_loops)

(* ⦃P1⦄ tcontra loops *)
  have "⦃P1⦄ tcontra ↑" 
    unfolding tcontra_def
    by (rule Hoare_plus_unhalt[OF first second H_composable])

  with assms show "False"
    unfolding P1_def
    unfolding  TMC_has_num_res_def
    unfolding Hoare_halt_def Hoare_unhalt_def
    by (auto simp add: tape_of_list_def)
qed

text ‹
  Thus ‹False› is derivable.
›

lemma false: "False"
  using tcontra_halt tcontra_unhalt 
  by auto

end (* locale uncomputable *)

end