6 header {* Undeciablity of the {\em Halting problem} *} |
6 header {* Undeciablity of the {\em Halting problem} *} |
7 |
7 |
8 theory uncomputable |
8 theory uncomputable |
9 imports Main turing_hoare |
9 imports Main turing_hoare |
10 begin |
10 begin |
|
11 |
|
12 declare tm_comp.simps [simp del] |
|
13 declare adjust.simps[simp del] |
|
14 declare shift.simps[simp del] |
|
15 declare tm_wf.simps[simp del] |
|
16 declare step.simps[simp del] |
|
17 declare steps.simps[simp del] |
|
18 |
|
19 |
|
20 lemma numeral: |
|
21 shows "1 = Suc 0" |
|
22 and "2 = Suc 1" |
|
23 and "3 = Suc 2" |
|
24 and "4 = Suc 3" |
|
25 and "5 = Suc 4" |
|
26 and "6 = Suc 5" by arith+ |
|
27 |
|
28 |
11 |
29 |
12 text {* |
30 text {* |
13 The {\em Copying} TM, which duplicates its input. |
31 The {\em Copying} TM, which duplicates its input. |
14 *} |
32 *} |
15 |
33 |
49 else if s = 4 then inv_init4 x (l, r) |
67 else if s = 4 then inv_init4 x (l, r) |
50 else False)" |
68 else False)" |
51 |
69 |
52 declare inv_init.simps[simp del] |
70 declare inv_init.simps[simp del] |
53 |
71 |
54 lemma numeral_4_eq_4: "4 = Suc 3" |
|
55 by arith |
|
56 |
72 |
57 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
73 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
58 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
74 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
59 apply(rule_tac x = "Suc i" in exI, simp) |
75 apply(rule_tac x = "Suc i" in exI, simp) |
60 done |
76 done |
61 |
77 |
62 lemma inv_init_step: |
78 lemma inv_init_step: |
63 "\<lbrakk>inv_init x cf; x > 0\<rbrakk> |
79 "\<lbrakk>inv_init x cf; x > 0\<rbrakk> |
64 \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))" |
80 \<Longrightarrow> inv_init x (step cf (tcopy_init, 0))" |
|
81 unfolding tcopy_init_def |
65 apply(case_tac cf) |
82 apply(case_tac cf) |
66 apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2 |
83 apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits) |
67 numeral_3_eq_3 numeral_4_eq_4 split: if_splits) |
|
68 apply(case_tac "hd c", auto simp: inv_init.simps) |
84 apply(case_tac "hd c", auto simp: inv_init.simps) |
69 apply(case_tac c, simp_all) |
85 apply(case_tac c, simp_all) |
70 done |
86 done |
71 |
87 |
72 lemma inv_init_steps: |
88 lemma inv_init_steps: |
135 steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE" |
151 steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE" |
136 using a |
152 using a |
137 proof(simp) |
153 proof(simp) |
138 assume "inv_init x (s, l, r)" "0 < s" |
154 assume "inv_init x (s, l, r)" "0 < s" |
139 thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE" |
155 thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE" |
140 apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2 |
156 apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral |
141 numeral_3_eq_3 numeral_4_eq_4 split: if_splits) |
157 split: if_splits) |
142 apply(case_tac r, auto, case_tac a, auto) |
158 apply(case_tac r, auto, case_tac a, auto) |
143 done |
159 done |
144 qed |
160 qed |
145 qed |
161 qed |
146 qed |
162 qed |
252 inv_loop6.simps[simp del] |
268 inv_loop6.simps[simp del] |
253 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR" |
269 lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR" |
254 apply(case_tac t, auto) |
270 apply(case_tac t, auto) |
255 done |
271 done |
256 |
272 |
257 lemma numeral_5_eq_5: "5 = Suc 4" by arith |
|
258 |
|
259 lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith |
|
260 |
273 |
261 lemma [simp]: "inv_loop1 x (b, []) = False" |
274 lemma [simp]: "inv_loop1 x (b, []) = False" |
262 by(simp add: inv_loop1.simps) |
275 by(simp add: inv_loop1.simps) |
263 |
276 |
264 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
277 lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])" |
470 |
483 |
471 lemma inv_loop_step: |
484 lemma inv_loop_step: |
472 "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> |
485 "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> |
473 \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))" |
486 \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))" |
474 apply(case_tac cf, case_tac c, case_tac [2] aa) |
487 apply(case_tac cf, case_tac c, case_tac [2] aa) |
475 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2 |
488 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits) |
476 numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits) |
|
477 done |
489 done |
478 |
490 |
479 lemma inv_loop_steps: |
491 lemma inv_loop_steps: |
480 "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> |
492 "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> |
481 \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)" |
493 \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)" |
646 done |
658 done |
647 hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE" |
659 hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE" |
648 using h |
660 using h |
649 apply(case_tac r', case_tac [2] a) |
661 apply(case_tac r', case_tac [2] a) |
650 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def |
662 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def |
651 numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 |
663 numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits) |
652 numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_def split: if_splits) |
|
653 done |
664 done |
654 thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), |
665 thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), |
655 steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE" |
666 steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE" |
656 using d |
667 using d |
657 apply(simp add: step_red) |
668 apply(simp add: step_red) |
860 lemma inv_end_step: |
871 lemma inv_end_step: |
861 "\<lbrakk>x > 0; |
872 "\<lbrakk>x > 0; |
862 inv_end x cf\<rbrakk> |
873 inv_end x cf\<rbrakk> |
863 \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))" |
874 \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))" |
864 apply(case_tac cf, case_tac c, case_tac [2] aa) |
875 apply(case_tac cf, case_tac c, case_tac [2] aa) |
865 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2 |
876 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits) |
866 numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits) |
|
867 done |
877 done |
868 |
878 |
869 lemma inv_end_steps: |
879 lemma inv_end_steps: |
870 "\<lbrakk>x > 0; inv_end x cf\<rbrakk> |
880 "\<lbrakk>x > 0; inv_end x cf\<rbrakk> |
871 \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)" |
881 \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)" |
935 apply(drule_tac stp = n in inv_end_steps, auto) |
945 apply(drule_tac stp = n in inv_end_steps, auto) |
936 done |
946 done |
937 hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE" |
947 hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE" |
938 apply(case_tac r', case_tac [2] a) |
948 apply(case_tac r', case_tac [2] a) |
939 apply(auto simp: inv_end.simps step.simps tcopy_end_def |
949 apply(auto simp: inv_end.simps step.simps tcopy_end_def |
940 numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4 |
950 numeral end_LE_def lex_triple_def lex_pair_def split: if_splits) |
941 numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits) |
|
942 done |
951 done |
943 thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), |
952 thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), |
944 steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE" |
953 steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE" |
945 using d |
954 using d |
946 by simp |
955 by simp |
1035 lemma dither_halt_rs: |
1044 lemma dither_halt_rs: |
1036 "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp = |
1045 "\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp = |
1037 (0, Bk\<up>m, [Oc, Oc])" |
1046 (0, Bk\<up>m, [Oc, Oc])" |
1038 apply(rule_tac x = "Suc (Suc (Suc 0))" in exI) |
1047 apply(rule_tac x = "Suc (Suc (Suc 0))" in exI) |
1039 apply(simp add: dither_def steps.simps |
1048 apply(simp add: dither_def steps.simps |
1040 step.simps fetch.simps numeral_2_eq_2) |
1049 step.simps fetch.simps numeral) |
1041 done |
1050 done |
1042 |
1051 |
1043 lemma dither_unhalt_state: |
1052 lemma dither_unhalt_state: |
1044 "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = |
1053 "(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = |
1045 (Suc 0, Bk\<up>m, [Oc])) \<or> |
1054 (Suc 0, Bk\<up>m, [Oc])) \<or> |
1046 (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))" |
1055 (steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))" |
1047 apply(induct stp, simp add: steps.simps) |
1056 apply(induct stp, simp add: steps.simps) |
1048 apply(simp add: step_red, auto) |
1057 apply(simp add: step_red, auto) |
1049 apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2) |
1058 apply(auto simp: step.simps fetch.simps dither_def numeral) |
1050 done |
1059 done |
1051 |
1060 |
1052 lemma dither_unhalt_rs: |
1061 lemma dither_unhalt_rs: |
1053 "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)" |
1062 "\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)" |
1054 using dither_unhalt_state[of m stp] |
1063 using dither_unhalt_state[of m stp] |
1322 apply(auto simp: haltP_def Hoare_def) |
1331 apply(auto simp: haltP_def Hoare_def) |
1323 apply(erule_tac x = n in allE) |
1332 apply(erule_tac x = n in allE) |
1324 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1333 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1325 apply(simp, auto) |
1334 apply(simp, auto) |
1326 apply(erule_tac x = nd in allE, erule_tac x = 2 in allE) |
1335 apply(erule_tac x = nd in allE, erule_tac x = 2 in allE) |
1327 apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv) |
1336 apply(simp add: numeral replicate_Suc tape_of_nl_abv) |
1328 apply(erule_tac x = 0 in allE, simp) |
1337 apply(erule_tac x = 0 in allE, simp) |
1329 done |
1338 done |
1330 qed |
1339 qed |
1331 |
1340 |
1332 |
1341 |
1333 lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)] |
1342 |
1334 \<Longrightarrow> \<not> haltP (tcontra H, 0) [code (tcontra H)]" |
1343 |
|
1344 lemma h_uh: |
|
1345 assumes "haltP (tcontra H, 0) [code (tcontra H)]" |
|
1346 shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]" |
1335 proof(simp only: tcontra_def) |
1347 proof(simp only: tcontra_def) |
1336 let ?tcontr = "(tcopy |+| H) |+| dither" |
1348 let ?tcontr = "(tcopy |+| H) |+| dither" |
1337 let ?cn = "Suc (code ?tcontr)" |
1349 let ?cn = "Suc (code ?tcontr)" |
1338 let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))" |
1350 let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))" |
1339 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1351 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1340 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1352 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1341 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1353 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1342 let ?P3 = ?Q2 |
1354 let ?P3 = ?Q2 |
1343 assume h: "haltP (?tcontr, 0) [code ?tcontr]" |
|
1344 have "{?P1} ?tcontr \<up>" |
1355 have "{?P1} ?tcontr \<up>" |
1345 proof(rule_tac Hoare_plus_unhalt, auto) |
1356 proof(rule_tac Hoare_plus_unhalt, auto) |
1346 show "?Q2 \<mapsto> ?P3" |
1357 show "?Q2 \<mapsto> ?P3" |
1347 apply(simp add: assert_imp_def) |
1358 apply(simp add: assert_imp_def) |
1348 done |
1359 done |
1388 thus "False" |
1400 thus "False" |
1389 using dither_unhalt_rs[of nd n] |
1401 using dither_unhalt_rs[of nd n] |
1390 by simp |
1402 by simp |
1391 qed |
1403 qed |
1392 qed |
1404 qed |
1393 thus "\<not> True" |
1405 thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]" |
1394 using h |
1406 using assms |
|
1407 unfolding tcontra_def |
1395 apply(auto simp: haltP_def Hoare_unhalt_def) |
1408 apply(auto simp: haltP_def Hoare_unhalt_def) |
1396 apply(erule_tac x = n in allE) |
1409 apply(erule_tac x = n in allE) |
1397 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1410 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1398 apply(simp add: tape_of_nl_abv) |
1411 apply(simp add: tape_of_nl_abv) |
1399 done |
1412 done |
1400 qed |
1413 qed |
1401 |
1414 |
|
1415 |
1402 text {* |
1416 text {* |
1403 @{text "False"} is finally derived. |
1417 @{text "False"} is finally derived. |
1404 *} |
1418 *} |
1405 |
1419 |
1406 lemma false: "False" |
1420 lemma false: "False" |
1407 using uh_h h_uh |
1421 using uh_h h_uh |
1408 by auto |
1422 by auto |
|
1423 |
1409 end |
1424 end |
1410 |
1425 |
1411 end |
1426 end |
1412 |
1427 |