--- a/thys/uncomputable.thy Wed Jan 23 15:06:32 2013 +0100
+++ b/thys/uncomputable.thy Wed Jan 23 15:33:26 2013 +0100
@@ -1037,33 +1037,52 @@
The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
terminate.
*}
+
definition dither :: "instr list"
where
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
-lemma dither_halt_rs:
- "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp =
- (0, Bk\<up>m, [Oc, Oc])"
-apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
-apply(simp add: dither_def steps.simps
- step.simps fetch.simps numeral)
-done
-
lemma dither_unhalt_state:
- "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp =
- (Suc 0, Bk\<up>m, [Oc])) \<or>
- (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
- apply(induct stp, simp add: steps.simps)
- apply(simp add: step_red, auto)
+ "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
+ (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
+ apply(induct stp)
+ apply(simp add: steps.simps)
+ apply(simp add: step_red)
apply(auto simp: step.simps fetch.simps dither_def numeral)
done
lemma dither_unhalt_rs:
- "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"
+ shows "\<not> is_final (steps0 (1, Bk \<up> m, [Oc]) dither stp)"
using dither_unhalt_state[of m stp]
+by auto
+
+lemma dither_loops:
+ shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>"
+apply(rule Hoare_unhaltI)
+using dither_unhalt_rs
apply(auto)
done
+lemma dither_halt_rs:
+ "\<exists>stp. steps0 (Suc 0, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])"
+unfolding dither_def
+apply(rule_tac x = "3" in exI)
+apply(simp add: steps.simps step.simps fetch.simps numeral)
+done
+
+definition
+ "dither_halt_inv \<equiv> (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])"
+
+lemma dither_halts:
+ shows "{dither_halt_inv} dither {dither_halt_inv}"
+unfolding dither_halt_inv_def
+apply(rule HoareI)
+using dither_halt_rs
+apply(auto)
+by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
+
+
+
section {*
The final diagnal arguments to show the undecidability of Halting problem.
*}
@@ -1250,29 +1269,15 @@
qed
qed
+(* TM that produces the contradiction *)
definition tcontra :: "instr list \<Rightarrow> instr list"
where
"tcontra h \<equiv> (tcopy |+| h) |+| dither"
-declare replicate_Suc[simp del]
-
-lemma dither_loops:
- shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>"
-apply(rule Hoare_unhaltI)
-apply(auto intro!: dither_unhalt_rs)
-done
-
-lemma dither_halts:
- shows
- "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])} dither {(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])}"
-apply(rule HoareI)
-using dither_halt_rs
-apply(auto)
-by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
lemma uh_h:
assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]"
- shows "haltP0 (tcontra H) [code (tcontra H)]"
+ shows "False"
proof -
(* code of tcontra *)
def code_tcontra \<equiv> "(code (tcontra H))"
@@ -1282,7 +1287,7 @@
(* invariants *)
def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+ def P3 \<equiv> dither_halt_inv
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1316,11 +1321,11 @@
using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
by (auto)
then show "{P2} H {P3}"
- unfolding P2_def P3_def
+ unfolding P2_def P3_def dither_halt_inv_def
unfolding Hoare_def
apply(auto)
apply(rule_tac x = n in exI)
- apply(simp add: replicate_Suc)
+ apply(simp)
done
qed (simp)
@@ -1332,8 +1337,8 @@
have "{P1} (tcontra H) {P3}" unfolding tcontra_def
by (rule Hoare_plus_halt_simple[OF first second H_wf])
- with assms' have "False"
- unfolding P1_def P3_def code_tcontra_def
+ with assms' show "False"
+ unfolding P1_def P3_def dither_halt_inv_def code_tcontra_def
unfolding haltP_def
unfolding Hoare_def
apply(auto)
@@ -1343,13 +1348,11 @@
apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
apply(simp)
by (smt replicate_0 replicate_Suc)
- then show "haltP0 (tcontra H) [code (tcontra H)]"
- by blast
qed
lemma h_uh:
assumes "haltP0 (tcontra H) [code (tcontra H)]"
- shows "\<not> haltP0 (tcontra H) [code (tcontra H)]"
+ shows "False"
proof -
(* code of tcontra *)
def code_tcontra \<equiv> "(code (tcontra H))"
@@ -1397,7 +1400,7 @@
unfolding Hoare_def
apply(auto)
apply(rule_tac x = n in exI)
- apply(simp add: replicate_Suc)
+ apply(simp)
done
qed (simp)
@@ -1409,13 +1412,11 @@
have "{P1} (tcontra H) \<up>" unfolding tcontra_def
by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
- with assms have "False"
+ with assms show "False"
unfolding haltP_def
unfolding P1_def code_tcontra_def
unfolding Hoare_unhalt_def
by (auto, metis is_final_eq)
- then show "\<not> haltP0 (tcontra H) [code_tcontra]"
- by blast
qed
@@ -1426,10 +1427,12 @@
*}
lemma false: "False"
-using uh_h h_uh
-by auto
+using uh_h h_uh by auto
end
+declare replicate_Suc[simp del]
+
+
end