# HG changeset patch
# User nipkow
# Date 1733424293 -3600
# Node ID 41b387d477398579652844c92f1a98982e500ea6
# Parent  92a3017f7d1a499666acfbd1d59d9b4b5bc33051
added Halting problem theory

diff -r 92a3017f7d1a -r 41b387d47739 src/HOL/IMP/Halting.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Halting.thy	Thu Dec 05 19:44:53 2024 +0100
@@ -0,0 +1,68 @@
+(*
+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
diff -r 92a3017f7d1a -r 41b387d47739 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Dec 05 15:49:48 2024 +0100
+++ b/src/HOL/ROOT	Thu Dec 05 19:44:53 2024 +0100
@@ -268,6 +268,7 @@
     Procs_Stat_Vars_Stat
     C_like
     OO
+    Halting
   document_files "root.bib" "root.tex"
 
 session "HOL-IMPP" in IMPP = HOL +