1042 assume "0 < x" |
1042 assume "0 < x" |
1043 thus "{inv_end1 x} tcopy_end {inv_end0 x}" |
1043 thus "{inv_end1 x} tcopy_end {inv_end0 x}" |
1044 by(erule_tac end_correct) |
1044 by(erule_tac end_correct) |
1045 qed |
1045 qed |
1046 |
1046 |
1047 section {* |
1047 abbreviation |
1048 The {\em Dithering} Turing Machine |
1048 "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)" |
1049 *} |
1049 abbreviation |
|
1050 "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[n, n::nat]>)" |
|
1051 |
|
1052 lemma tcopy_correct2: |
|
1053 shows "{pre_tcopy n} tcopy {post_tcopy n}" |
|
1054 proof - |
|
1055 have "{inv_init1 (Suc n)} tcopy {inv_end0 (Suc n)}" |
|
1056 by (rule tcopy_correct1) (simp) |
|
1057 moreover |
|
1058 have "pre_tcopy n \<mapsto> inv_init1 (Suc n)" |
|
1059 by (simp add: assert_imp_def tape_of_nl_abv) |
|
1060 moreover |
|
1061 have "inv_end0 (Suc n) \<mapsto> post_tcopy n" |
|
1062 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
|
1063 ultimately |
|
1064 show "{pre_tcopy n} tcopy {post_tcopy n}" |
|
1065 by (rule Hoare_weak) |
|
1066 qed |
|
1067 |
|
1068 |
|
1069 section {* The {\em Dithering} Turing Machine *} |
1050 |
1070 |
1051 text {* |
1071 text {* |
1052 The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will |
1072 The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will |
1053 terminate. |
1073 terminate. |
1054 *} |
1074 *} |
1175 done |
1195 done |
1176 qed |
1196 qed |
1177 |
1197 |
1178 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb" |
1198 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb" |
1179 apply(auto simp: tinres_def replicate_add[THEN sym]) |
1199 apply(auto simp: tinres_def replicate_add[THEN sym]) |
1180 apply(case_tac "nb \<ge> n") |
1200 apply(case_tac "nb > n") |
1181 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1201 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1182 apply arith |
1202 apply arith |
1183 apply(drule_tac length_eq, simp) |
1203 by (metis Nil_is_append_conv add_diff_inverse append_assoc nat_add_commute replicate_0 replicate_add |
1184 done |
1204 self_append_conv2) |
1185 |
|
1186 |
1205 |
1187 text {* |
1206 text {* |
1188 The following locale specifies that TM @{text "H"} can be used to solve |
1207 The following locale specifies that TM @{text "H"} can be used to solve |
1189 the {\em Halting Problem} and @{text "False"} is going to be derived |
1208 the {\em Halting Problem} and @{text "False"} is going to be derived |
1190 under this locale. Therefore, the undecidability of {\em Halting Problem} |
1209 under this locale. Therefore, the undecidability of {\em Halting Problem} |
1309 |
1328 |
1310 (* {P1} (tcopy |+| H) {P3} *) |
1329 (* {P1} (tcopy |+| H) {P3} *) |
1311 have first: "{P1} (tcopy |+| H) {P3}" |
1330 have first: "{P1} (tcopy |+| H) {P3}" |
1312 proof (cases rule: Hoare_plus_halt_simple) |
1331 proof (cases rule: Hoare_plus_halt_simple) |
1313 case A_halt (* of tcopy *) |
1332 case A_halt (* of tcopy *) |
1314 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1333 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1315 by (rule tcopy_correct1) (simp) |
1334 by (rule tcopy_correct2) |
1316 moreover |
|
1317 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
|
1318 by (simp add: assert_imp_def tape_of_nl_abv) |
|
1319 moreover |
|
1320 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def |
|
1321 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
|
1322 ultimately |
|
1323 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
|
1324 next |
1335 next |
1325 case B_halt |
1336 case B_halt |
1326 obtain n i |
1337 obtain n i |
1327 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])" |
1338 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])" |
1328 using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |
1339 using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |
1379 |
1390 |
1380 (* {P1} (tcopy |+| H) {P3} *) |
1391 (* {P1} (tcopy |+| H) {P3} *) |
1381 have first: "{P1} (tcopy |+| H) {P3}" |
1392 have first: "{P1} (tcopy |+| H) {P3}" |
1382 proof (cases rule: Hoare_plus_halt_simple) |
1393 proof (cases rule: Hoare_plus_halt_simple) |
1383 case A_halt (* of tcopy *) |
1394 case A_halt (* of tcopy *) |
1384 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1395 show "{P1} tcopy {P2}" unfolding P1_def P2_def |
1385 by (rule tcopy_correct1) (simp) |
1396 by (rule tcopy_correct2) |
1386 moreover |
|
1387 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
|
1388 by (simp add: assert_imp_def tape_of_nl_abv) |
|
1389 moreover |
|
1390 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def |
|
1391 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
|
1392 ultimately |
|
1393 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
|
1394 next |
1397 next |
1395 case B_halt |
1398 case B_halt |
1396 obtain n i |
1399 obtain n i |
1397 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])" |
1400 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])" |
1398 using h_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |
1401 using h_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |