1073 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]" |
1073 "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]" |
1074 |
1074 |
1075 abbreviation |
1075 abbreviation |
1076 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]" |
1076 "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]" |
1077 |
1077 |
1078 lemma dither_unhalt_state: |
1078 lemma dither_loops_aux: |
1079 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1079 "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or> |
1080 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1080 (steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))" |
1081 apply(induct stp) |
1081 apply(induct stp) |
1082 apply(simp add: steps.simps) |
1082 apply(auto simp: steps.simps step.simps dither_def numeral) |
1083 apply(simp add: step_red) |
|
1084 apply(auto simp: step.simps fetch.simps dither_def numeral) |
|
1085 done |
1083 done |
1086 |
|
1087 lemma dither_unhalt_rs: |
|
1088 shows "\<not> is_final (steps0 (1, Bk \<up> m, [Oc]) dither stp)" |
|
1089 using dither_unhalt_state[of m stp] |
|
1090 by auto |
|
1091 |
1084 |
1092 lemma dither_loops: |
1085 lemma dither_loops: |
1093 shows "{dither_unhalt_inv} dither \<up>" |
1086 shows "{dither_unhalt_inv} dither \<up>" |
1094 apply(rule Hoare_unhaltI) |
1087 apply(rule Hoare_unhaltI) |
1095 using dither_unhalt_rs |
1088 using dither_loops_aux |
1096 apply(auto) |
1089 apply(auto simp add: numeral) |
1097 done |
1090 by (metis Suc_neq_Zero is_final_eq) |
1098 |
1091 |
1099 lemma dither_halt_rs: |
1092 |
1100 "\<exists>stp. steps0 (1, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])" |
1093 lemma dither_halts_aux: |
|
1094 shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])" |
1101 unfolding dither_def |
1095 unfolding dither_def |
1102 apply(rule_tac x = "3" in exI) |
1096 by (simp add: steps.simps step.simps numeral) |
1103 apply(simp add: steps.simps step.simps fetch.simps numeral) |
|
1104 done |
|
1105 |
|
1106 |
1097 |
1107 lemma dither_halts: |
1098 lemma dither_halts: |
1108 shows "{dither_halt_inv} dither {dither_halt_inv}" |
1099 shows "{dither_halt_inv} dither {dither_halt_inv}" |
1109 apply(rule Hoare_haltI) |
1100 apply(rule Hoare_haltI) |
1110 using dither_halt_rs |
1101 using dither_halts_aux |
1111 apply(auto) |
1102 apply(auto) |
1112 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) |
1103 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) |
1113 |
1104 |
1114 |
1105 |
1115 |
1106 |
1116 section {* |
1107 section {* The diagnal argument below shows the undecidability of Halting problem *} |
1117 The final diagnal arguments to show the undecidability of Halting problem. |
|
1118 *} |
|
1119 |
1108 |
1120 text {* |
1109 text {* |
1121 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
1110 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
1122 and the final configuration is standard. |
1111 and the final configuration is standard. |
1123 *} |
1112 *} |
1124 |
1113 |
1125 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool" |
1114 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool" |
1126 where |
1115 where |
1127 "haltP p lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))" |
1116 "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a, Oc \<up> b @ Bk \<up> c)" |
1128 |
|
1129 |
1117 |
1130 abbreviation |
1118 abbreviation |
1131 "haltP0 p lm \<equiv> haltP (p, 0) lm" |
1119 "haltP0 p lm \<equiv> haltP (p, 0) lm" |
1132 |
1120 |
1133 lemma [intro, simp]: "tm_wf0 tcopy" |
1121 lemma [intro, simp]: "tm_wf0 tcopy" |