Theory TuringDecidable

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

section ‹Turing Decidability›

theory TuringDecidable
  imports
    OneStrokeTM
    Turing_HaltingConditions
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]
*)

subsection ‹Turing Decidable Sets and Relations of natural numbers›

text ‹We use lists of natural numbers in order to model tuples of
 arity @{term k} of natural numbers,
 where @{term "0 ≤ (k::nat)"}. 
›

(*
 For a relation R of @⦃term k⦄-ary tuples use a set nls of nat lists,
 where each of its elements nl (which is a nat list) has length k.
    
     (n1, ... , nk) ∈ R ⟷ [<[n1, ... , nk]>] ∈ nls .
  
 For a plain set of natural numbers S simply use a set of singleton nat lists nls
 where

      n ∈ S ⟷ [<n>] ∈ nls.
*)

text ‹Now, we define the notion of {\em Turing Decidable Sets and Relations}.
In our definition, we directly relate decidability of sets and relations to Turing machines
and do not adhere to the formal concept of a characteristic function.

However, the notion of a characteristic function is introduced in the theory about Turing
computable functions.
›

definition turing_decidable :: "(nat list) set ⇒ bool"
  where
    "turing_decidable nls ≡ (∃D. (∀nl. 
         (nl ∈ nls ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk↑ l))⦄)
       ∧ (nl ∉ nls ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk↑ l))⦄)
     ))"

(* This is for documentation and explanation: turing_decidable_unfolded_into_TMC_yields_conditions *)

lemma turing_decidable_unfolded_into_TMC_yields_conditions:
"turing_decidable nls ≡ (∃D. (∀nl. 
         (nl ∈ nls ⟶ TMC_yields_num_res D nl (1::nat) )
       ∧ (nl ∉ nls ⟶ TMC_yields_num_res D nl (0::nat) )
     ))"
  unfolding TMC_yields_num_res_unfolded_into_Hoare_halt
  by (simp add: turing_decidable_def)

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

subsection ‹Examples for decidable sets of natural numbers›

text ‹Using the machine OneStrokeTM as a decider
we are able to proof the decidability of the empty set.
Moreover, in the theory about Halting Problems, we will show that there are undecidable sets as well.
Thus, the notion of Turing Decidability is not a trivial concept.
›

lemma turing_decidable_empty_set_iff:
  "turing_decidable {} = (∃D. ∀(nl:: nat list).
        ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, [Oc] @ Bk ↑l))⦄)"
  unfolding turing_decidable_def
  by (simp add: tape_of_nat_def)

theorem turing_decidable_empty_set: "turing_decidable {}"
  by (rule turing_decidable_empty_set_iff[THEN iffD2])
     (blast intro: tm_onestroke_total_correctness)

(* For demo in classes *)
(*
lemma tm_onestroke_total_correctness':
  "∀nl. TMC_yields_num_res tm_onestroke nl (0::nat)"
  unfolding TMC_yields_num_res_unfolded_into_Hoare_halt
  using tm_onestroke_total_correctness by (simp add: tape_of_nat_def)

theorem turing_decidable_empty_set':
  "(∀nl. 
             (nl ∈ {} ⟶ TMC_yields_num_res tm_onestroke nl (1::nat) )
           ∧ (nl ∉ {} ⟶ TMC_yields_num_res tm_onestroke nl (0::nat) )
         )"
  unfolding TMC_yields_num_res_unfolded_into_Hoare_halt
proof -
  show "∀nl. (nl ∈ {} ⟶ ⦃λtap. tap = ([], <nl::nat list>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄) ∧
               (nl ∉ {} ⟶ ⦃λtap. tap = ([], <nl::nat list>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄)"
  proof
    fix nl:: "nat list"
    show "(nl ∈ {} ⟶ ⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄) ∧
          (nl ∉ {} ⟶ ⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄)"
    proof
      show "nl ∈ {} ⟶ ⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄"
      proof
        assume "nl ∈ {}" (* nothing can ever be an element of the empty set {}, thus contradiction *)
        then have False by auto
        then show "⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄" by auto
      qed
    next
      show "nl ∉ {} ⟶ ⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄"
      proof
        assume "nl ∉ {}"
        have "∀nl.⦃λtap. tap = ([], <nl::nat list>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄"
          using TMC_yields_num_res_unfolded_into_Hoare_halt tm_onestroke_total_correctness' by blast
        then show "⦃λtap. tap = ([], <nl>)⦄ tm_onestroke ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄" by auto
      qed
    qed
  qed
qed

corollary "turing_decidable {}"
  unfolding turing_decidable_unfolded_into_TMC_yields_conditions
  using turing_decidable_empty_set' by auto
*)

(* ---------------------------------------------------- *)
(* ENHANCE: add a means for turing_semi_decidable       *)
(* ---------------------------------------------------- *)

(* ---------------------------------------------------- *)
(* ENHANCE: add a means for dove-tailing                *)
(* ---------------------------------------------------- *)

(* ---------------------------------------------------- *)
(* ENHANCE: prove advanced theorems about decidability  *)
(* ---------------------------------------------------- *)
(* - Step counter theorem ;aka (s,m,n) theorem          *)
(* - Rice's theorem for Turing Machines                 *)
(* ---------------------------------------------------- *)

end