985 |
985 |
986 |
986 |
987 section {* The diagnal argument below shows the undecidability of Halting problem *} |
987 section {* The diagnal argument below shows the undecidability of Halting problem *} |
988 |
988 |
989 text {* |
989 text {* |
990 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
990 @{text "halts tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
991 and the final configuration is standard. |
991 and the final configuration is standard. |
992 *} |
992 *} |
993 |
993 |
994 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
994 definition halts :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
995 where |
995 where |
996 "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}" |
996 "halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}" |
997 |
997 |
998 lemma [intro, simp]: "tm_wf0 tcopy" |
998 lemma [intro, simp]: "tm_wf0 tcopy" |
999 by (auto simp: tcopy_def) |
999 by (auto simp: tcopy_def) |
1000 |
1000 |
1001 lemma [intro, simp]: "tm_wf0 dither" |
1001 lemma [intro, simp]: "tm_wf0 dither" |
1019 assumes h_wf[intro]: "tm_wf0 H" |
1019 assumes h_wf[intro]: "tm_wf0 H" |
1020 -- {* |
1020 -- {* |
1021 The following two assumptions specifies that @{text "H"} does solve the Halting problem. |
1021 The following two assumptions specifies that @{text "H"} does solve the Halting problem. |
1022 *} |
1022 *} |
1023 and h_case: |
1023 and h_case: |
1024 "\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}" |
1024 "\<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>))}" |
1025 and nh_case: |
1025 and nh_case: |
1026 "\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}" |
1026 "\<And> M ns. \<not> halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}" |
1027 begin |
1027 begin |
1028 |
1028 |
1029 (* invariants for H *) |
1029 (* invariants for H *) |
1030 abbreviation (input) |
1030 abbreviation (input) |
1031 "pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)" |
1031 "pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)" |
1036 abbreviation (input) |
1036 abbreviation (input) |
1037 "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)" |
1037 "post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)" |
1038 |
1038 |
1039 |
1039 |
1040 lemma H_halt_inv: |
1040 lemma H_halt_inv: |
1041 assumes "\<not> haltP M ns" |
1041 assumes "\<not> halts M ns" |
1042 shows "{pre_H_inv M ns} H {post_H_halt_inv}" |
1042 shows "{pre_H_inv M ns} H {post_H_halt_inv}" |
1043 using assms nh_case by auto |
1043 using assms nh_case by auto |
1044 |
1044 |
1045 lemma H_unhalt_inv: |
1045 lemma H_unhalt_inv: |
1046 assumes "haltP M ns" |
1046 assumes "halts M ns" |
1047 shows "{pre_H_inv M ns} H {post_H_unhalt_inv}" |
1047 shows "{pre_H_inv M ns} H {post_H_unhalt_inv}" |
1048 using assms h_case by auto |
1048 using assms h_case by auto |
1049 |
1049 |
1050 (* TM that produces the contradiction and its code *) |
1050 (* TM that produces the contradiction and its code *) |
1051 |
1051 |
1054 abbreviation |
1054 abbreviation |
1055 "code_tcontra \<equiv> code tcontra" |
1055 "code_tcontra \<equiv> code tcontra" |
1056 |
1056 |
1057 (* assume tcontra does not halt on its code *) |
1057 (* assume tcontra does not halt on its code *) |
1058 lemma tcontra_unhalt: |
1058 lemma tcontra_unhalt: |
1059 assumes "\<not> haltP tcontra [code tcontra]" |
1059 assumes "\<not> halts tcontra [code tcontra]" |
1060 shows "False" |
1060 shows "False" |
1061 proof - |
1061 proof - |
1062 (* invariants *) |
1062 (* invariants *) |
1063 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)" |
1063 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)" |
1064 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" |
1064 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" |
1097 unfolding tcontra_def |
1097 unfolding tcontra_def |
1098 by (rule Hoare_plus_halt[OF first second H_wf]) |
1098 by (rule Hoare_plus_halt[OF first second H_wf]) |
1099 |
1099 |
1100 with assms show "False" |
1100 with assms show "False" |
1101 unfolding P1_def P3_def |
1101 unfolding P1_def P3_def |
1102 unfolding haltP_def |
1102 unfolding halts_def |
1103 unfolding Hoare_halt_def |
1103 unfolding Hoare_halt_def |
1104 apply(auto) |
1104 apply(auto) |
1105 apply(drule_tac x = n in spec) |
1105 apply(drule_tac x = n in spec) |
1106 apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n") |
1106 apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n") |
1107 apply(auto simp add: tape_of_nl_abv) |
1107 apply(auto simp add: tape_of_nl_abv) |
1108 by (metis append_Nil2 replicate_0) |
1108 by (metis append_Nil2 replicate_0) |
1109 qed |
1109 qed |
1110 |
1110 |
1111 (* asumme tcontra halts on its code *) |
1111 (* asumme tcontra halts on its code *) |
1112 lemma tcontra_halt: |
1112 lemma tcontra_halt: |
1113 assumes "haltP tcontra [code tcontra]" |
1113 assumes "halts tcontra [code tcontra]" |
1114 shows "False" |
1114 shows "False" |
1115 proof - |
1115 proof - |
1116 (* invariants *) |
1116 (* invariants *) |
1117 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)" |
1117 def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)" |
1118 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" |
1118 def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)" |