equal
deleted
inserted
replaced
1069 text {* |
1069 text {* |
1070 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
1070 @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"} |
1071 and the final configuration is standard. |
1071 and the final configuration is standard. |
1072 *} |
1072 *} |
1073 |
1073 |
1074 |
|
1075 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" ("< _ >" [0] 100) |
|
1076 where |
|
1077 "tape_of_nat_list [] = []" | |
|
1078 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
|
1079 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
|
1080 |
|
1081 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool" |
1074 definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool" |
1082 where |
1075 where |
1083 "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))" |
1076 "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))" |
1084 |
1077 |
1085 lemma [intro]: "tm_wf (tcopy, 0)" |
1078 lemma [intro]: "tm_wf (tcopy, 0)" |
1339 next |
1332 next |
1340 show "{?P2} (H, 0) {?Q2}" |
1333 show "{?P2} (H, 0) {?Q2}" |
1341 using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1334 using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1342 apply(auto) |
1335 apply(auto) |
1343 apply(rule_tac x = na in exI) |
1336 apply(rule_tac x = na in exI) |
1344 apply(simp add: replicate_Suc) |
1337 apply(simp add: replicate_Suc tape_of_nl_abv) |
1345 done |
1338 done |
1346 qed |
1339 qed |
1347 next |
1340 next |
1348 show "{?P3}(dither, 0){?Q3}" |
1341 show "{?P3}(dither, 0){?Q3}" |
1349 using Hoare_def |
1342 using Hoare_def |
1362 using h |
1355 using h |
1363 apply(auto simp: haltP_def Hoare_def) |
1356 apply(auto simp: haltP_def Hoare_def) |
1364 apply(erule_tac x = n in allE) |
1357 apply(erule_tac x = n in allE) |
1365 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1358 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1366 apply(simp, auto) |
1359 apply(simp, auto) |
1367 apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE) |
1360 apply(erule_tac x = nd in allE, erule_tac x = 2 in allE) |
1368 apply(simp add: numeral_2_eq_2 replicate_Suc) |
1361 apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv) |
|
1362 apply(erule_tac x = 0 in allE, simp) |
1369 done |
1363 done |
1370 qed |
1364 qed |
1371 |
1365 |
1372 |
1366 |
1373 lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)] |
1367 lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)] |
1414 next |
1408 next |
1415 show "{?P2} (H, 0) {?Q2}" |
1409 show "{?P2} (H, 0) {?Q2}" |
1416 using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1410 using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1417 apply(auto) |
1411 apply(auto) |
1418 apply(rule_tac x = na in exI) |
1412 apply(rule_tac x = na in exI) |
1419 apply(simp add: replicate_Suc) |
1413 apply(simp add: replicate_Suc tape_of_nl_abv) |
1420 done |
1414 done |
1421 qed |
1415 qed |
1422 next |
1416 next |
1423 show "{?P3}(dither, 0)" |
1417 show "{?P3}(dither, 0)" |
1424 using Hoare_unhalt_def |
1418 using Hoare_unhalt_def |
1432 qed |
1426 qed |
1433 thus "\<not> True" |
1427 thus "\<not> True" |
1434 using h |
1428 using h |
1435 apply(auto simp: haltP_def Hoare_unhalt_def) |
1429 apply(auto simp: haltP_def Hoare_unhalt_def) |
1436 apply(erule_tac x = n in allE) |
1430 apply(erule_tac x = n in allE) |
1437 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n", simp) |
1431 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
|
1432 apply(simp add: tape_of_nl_abv) |
1438 done |
1433 done |
1439 qed |
1434 qed |
1440 |
1435 |
1441 text {* |
1436 text {* |
1442 @{text "False"} is finally derived. |
1437 @{text "False"} is finally derived. |