--- a/thys/Uncomputable.thy Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Uncomputable.thy Wed Dec 19 16:10:58 2018 +0100
@@ -2,7 +2,7 @@
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)
-header {* Undeciablity of the Halting Problem *}
+chapter {* Undeciablity of the Halting Problem *}
theory Uncomputable
imports Turing_Hoare
@@ -19,6 +19,8 @@
and "8 = Suc 7"
and "9 = Suc 8"
and "10 = Suc 9"
+ and "11 = Suc 10"
+ and "12 = Suc 11"
by simp_all
text {* The Copying TM, which duplicates its input. *}
@@ -163,7 +165,7 @@
apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
apply(subgoal_tac "r = [Oc]")
apply(auto)
- by (metis cell.exhaust list.exhaust tl.simps(2))
+ by (metis cell.exhaust list.exhaust list.sel(3))
then
show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
using eq by (simp only: step_red)
@@ -596,7 +598,8 @@
qed
lemma loop_correct:
- shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"
+ assumes "0 < n"
+ shows "{inv_loop1 n} tcopy_loop {inv_loop0 n}"
using assms
proof(rule_tac Hoare_haltI)
fix l r
@@ -918,7 +921,7 @@
qed
abbreviation (input)
- "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"
+ "pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, Oc \<up> (Suc n))"
abbreviation (input)
"post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
@@ -928,11 +931,12 @@
have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
by (rule tcopy_correct1) (simp)
moreover
- have "pre_tcopy n = inv_begin1 (Suc n)"
- by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
+ have "pre_tcopy n = inv_begin1 (Suc n)"
+ by (auto)
moreover
- have "inv_end0 (Suc n) = post_tcopy n"
- by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)
+ have "inv_end0 (Suc n) = post_tcopy n"
+ unfolding fun_eq_iff
+ by (auto simp add: inv_end0.simps tape_of_nat_def tape_of_prod_def)
ultimately
show "{pre_tcopy n} tcopy {post_tcopy n}"
by simp
@@ -961,14 +965,14 @@
"(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(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
+ apply(auto simp: steps.simps step.simps dither_def numeral)
done
lemma dither_loops:
shows "{dither_unhalt_inv} dither \<up>"
apply(rule Hoare_unhaltI)
using dither_loops_aux
-apply(auto simp add: numeral tape_of_nat_abv)
+apply(auto simp add: numeral tape_of_nat_def)
by (metis Suc_neq_Zero is_final_eq)
lemma dither_halts_aux:
@@ -980,8 +984,8 @@
shows "{dither_halt_inv} dither {dither_halt_inv}"
apply(rule Hoare_haltI)
using dither_halts_aux
-apply(auto simp add: tape_of_nat_abv)
-by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
+apply(auto simp add: tape_of_nat_def)
+by (metis (lifting, mono_tags) holds_for.simps is_final_eq)
section {* The diagnal argument below shows the undecidability of Halting problem *}
@@ -1009,17 +1013,17 @@
*}
locale uncomputable =
- -- {* The coding function of TM, interestingly, the detailed definition of this
- funciton @{text "code"} does not affect the final result. *}
+ (* The coding function of TM, interestingly, the detailed definition of this
+ funciton @{text "code"} does not affect the final result. *)
fixes code :: "instr list \<Rightarrow> nat"
- -- {*
+ (*
The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
- *}
+ *)
and H :: "instr list"
assumes h_wf[intro]: "tm_wf0 H"
- -- {*
+ (*
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
- *}
+ *)
and h_case:
"\<And> M ns. halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
and nh_case:
@@ -1060,9 +1064,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
- def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
- def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
+ define P1 where "P1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
+ define P2 where "P2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
+ define P3 where "P3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1078,14 +1082,14 @@
have first: "{P1} (tcopy |+| H) {P3}"
proof (cases rule: Hoare_plus_halt)
case A_halt (* of tcopy *)
- show "{P1} tcopy {P2}" unfolding P1_def P2_def
+ show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
by (rule tcopy_correct)
next
case B_halt (* of H *)
show "{P2} H {P3}"
unfolding P2_def P3_def
using H_halt_inv[OF assms]
- by (simp add: tape_of_nat_pair tape_of_nl_abv)
+ by (simp add: tape_of_prod_def tape_of_list_def)
qed (simp)
(* {P3} dither {P3} *)
@@ -1104,7 +1108,7 @@
apply(auto)
apply(drule_tac x = n in spec)
apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
- apply(auto simp add: tape_of_nl_abv)
+ apply(auto simp add: tape_of_list_def)
by (metis append_Nil2 replicate_0)
qed
@@ -1114,9 +1118,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
- def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
- def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
+ define P1 where "P1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
+ define P2 where "P2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
+ define Q3 where "Q3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
(*
{P1} tcopy {P2} {P2} H {Q3}
@@ -1132,13 +1136,13 @@
have first: "{P1} (tcopy |+| H) {Q3}"
proof (cases rule: Hoare_plus_halt)
case A_halt (* of tcopy *)
- show "{P1} tcopy {P2}" unfolding P1_def P2_def
+ show "{P1} tcopy {P2}" unfolding P1_def P2_def tape_of_nat_def
by (rule tcopy_correct)
next
case B_halt (* of H *)
then show "{P2} H {Q3}"
unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
- by(simp add: tape_of_nat_pair tape_of_nl_abv)
+ by(simp add: tape_of_prod_def tape_of_list_def)
qed (simp)
(* {P3} dither loops *)
@@ -1154,7 +1158,7 @@
unfolding P1_def
unfolding halts_def
unfolding Hoare_halt_def Hoare_unhalt_def
- by (auto simp add: tape_of_nl_abv)
+ by (auto simp add: tape_of_list_def)
qed