src/HOL/IMP/Halting.thy

treat map_filter similar to list_all, list_ex, list_ex1

(*
Undecidability of the special Halting problem:
  Does a program applied to an encoding of itself terminate?
Author: Fabian Huch
*)

theory Halting
  imports "HOL-IMP.Big_Step"
begin

definition "halts c s \<equiv> (\<exists>s'. (c, s) \<Rightarrow> s')"

text \<open>A simple program that does not halt:\<close>
definition "loop \<equiv> WHILE Bc True DO SKIP"

lemma loop_never_halts[simp]: "\<not> halts loop s"
  unfolding halts_def
proof clarify
  fix s' assume "(loop, s) \<Rightarrow> s'"
  then show False
    by (induction loop s s' rule: big_step_induct) (simp_all add: loop_def)
qed

section \<open>Halting Problem\<close>

text \<open>
Given any encoding \<open>f\<close> (of programs to states), there is no Program \<open>H\<close> such that 
for all programs \<open>c\<close>, \<open>H\<close> terminates in a state \<open>s'\<close> which has at variable \<open>x\<close> the
answer whether \<open>c\<close> halts.\<close>

theorem halting: 
  "\<nexists>H. \<forall>c. \<exists>s'. (H, f c) \<Rightarrow> s' \<and> (halts c (f c) \<longleftrightarrow> s' x > 0)"
  (is "\<nexists>H. ?P H")
proof clarify
  fix H assume assm: "?P H"

  \<comment> \<open>inverted H: loops if input halts\<close>
  let ?inv_H = "H ;; IF Less (V x) (N 1) THEN SKIP ELSE loop" 

  \<comment> \<open>compute in \<open>s'\<close> whether inverted \<open>H\<close> halts when applied to itself\<close>
  obtain s' where 
    s'_def: "(H, f ?inv_H) \<Rightarrow> s'" and 
    s'_halts: "halts ?inv_H (f ?inv_H) \<longleftrightarrow> (s' x > 0)" 
    using assm by blast

  \<comment> \<open>contradiction: if it terminates, loop must have terminated; if not, SKIP must have looped!\<close>
  show False
  proof(cases "halts ?inv_H (f ?inv_H)")
    case True

    then have "halts (IF Less (V x) (N 1) THEN SKIP ELSE loop) s'"
      unfolding halts_def using big_step_determ s'_def by fast

    then have "halts loop s'"
      using s'_halts True halts_def by auto

    then show False by auto
  next
    case False

    then have "\<not> halts SKIP s'"
      using s'_def s'_halts halts_def by force

    then show False using halts_def by auto
  qed
qed

end