29 |
29 |
30 text {* |
30 text {* |
31 The {\em Copying} TM, which duplicates its input. |
31 The {\em Copying} TM, which duplicates its input. |
32 *} |
32 *} |
33 |
33 |
34 definition tcopy_init :: "instr list" |
34 definition |
|
35 tcopy_init :: "instr list" |
35 where |
36 where |
36 "tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2), |
37 "tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2), |
37 (W1, 3), (L, 4), (L, 4), (L, 0)]" |
38 (W1, 3), (L, 4), (L, 4), (L, 0)]" |
|
39 |
|
40 definition |
|
41 tcopy_loop :: "instr list" |
|
42 where |
|
43 "tcopy_loop \<equiv> [(R, 0), (R, 2), (R, 3), (W0, 2), |
|
44 (R, 3), (R, 4), (W1, 5), (R, 4), |
|
45 (L, 6), (L, 5), (L, 6), (L, 1)]" |
|
46 |
|
47 definition |
|
48 tcopy_end :: "instr list" |
|
49 where |
|
50 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
|
51 (R, 2), (R, 2), (L, 5), (W0, 4), |
|
52 (R, 0), (L, 5)]" |
|
53 |
|
54 definition |
|
55 tcopy :: "instr list" |
|
56 where |
|
57 "tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end" |
|
58 |
|
59 |
|
60 (* tcopy_init *) |
38 |
61 |
39 fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
62 fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
40 where |
63 where |
41 "inv_init1 x (l, r) = (l = [] \<and> r = Oc\<up>x )" |
64 "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x )" |
42 |
65 |
43 fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
66 fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
44 where |
67 where |
45 "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<up>i \<and> r = Oc\<up>j)" |
68 "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc\<up>j)" |
46 |
69 |
47 fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
70 fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
48 where |
71 where |
49 "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<up>x \<and> tl r = [])" |
72 "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])" |
50 |
73 |
51 fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
74 fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
52 where |
75 where |
53 "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc\<up>x \<and> r = [Bk, Oc]) \<or> (l = Oc\<up>(x - 1) \<and> r = [Oc, Bk, Oc])))" |
76 "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))" |
54 |
77 |
55 fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
78 fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
56 where |
79 where |
57 "inv_init0 x (l, r) = ((x > Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or> |
80 "inv_init0 x (l, r) = ((x > Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or> |
58 (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))" |
81 (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))" |
180 apply(rule_tac x = stp in exI) |
203 apply(rule_tac x = stp in exI) |
181 apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps) |
204 apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) stp)", simp add: inv_init.simps) |
182 done |
205 done |
183 qed |
206 qed |
184 |
207 |
185 definition tcopy_loop :: "instr list" |
208 |
186 where |
209 (* tcopy_loop *) |
187 "tcopy_loop \<equiv> [(R, 0), (R, 2), (R, 3), (W0, 2), |
|
188 (R, 3), (R, 4), (W1, 5), (R, 4), |
|
189 (L, 6), (L, 5), (L, 6), (L, 1)]" |
|
190 |
210 |
191 fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
211 fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
192 where |
212 where |
193 "inv_loop1_loop x (l, r) = |
213 "inv_loop1_loop x (l, r) = |
194 (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)" |
214 (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)" |
690 apply(rule_tac x = stp in exI) |
710 apply(rule_tac x = stp in exI) |
691 apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", |
711 apply(case_tac "(steps (Suc 0, l, r) (tcopy_loop, 0) stp)", |
692 simp add: inv_init.simps inv_loop.simps) |
712 simp add: inv_init.simps inv_loop.simps) |
693 done |
713 done |
694 qed |
714 qed |
|
715 |
|
716 |
|
717 (* tcopy_end *) |
695 |
718 |
696 definition tcopy_end :: "instr list" |
|
697 where |
|
698 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
|
699 (R, 2), (R, 2), (L, 5), (W0, 4), |
|
700 (R, 0), (L, 5)]" |
|
701 |
|
702 fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
719 fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
703 where |
720 where |
704 "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)" |
721 "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)" |
705 |
722 |
706 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
723 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
1158 using h |
1173 using h |
1159 apply(simp, simp, simp) |
1174 apply(simp, simp, simp) |
1160 done |
1175 done |
1161 qed |
1176 qed |
1162 |
1177 |
1163 lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys" |
|
1164 by auto |
|
1165 |
|
1166 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb" |
1178 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb" |
1167 apply(auto simp: tinres_def replicate_add[THEN sym]) |
1179 apply(auto simp: tinres_def replicate_add[THEN sym]) |
1168 apply(case_tac "nb \<ge> n") |
1180 apply(case_tac "nb \<ge> n") |
1169 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1181 apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add) |
1170 apply arith |
1182 apply arith |
1171 apply(drule_tac length_eq, simp) |
1183 apply(drule_tac length_eq, simp) |
1172 done |
1184 done |
1173 |
1185 |
1174 |
1186 |
1175 text {* |
1187 text {* |
1176 The following locale specifies that TM @{text "H"} can be used to solve |
1188 The following locale specifies that TM @{text "H"} can be used to solve |
1177 the {\em Halting Problem} and @{text "False"} is going to be derived |
1189 the {\em Halting Problem} and @{text "False"} is going to be derived |
1288 (* |
1300 (* |
1289 {P1} tcopy {P2} {P2} H {P3} |
1301 {P1} tcopy {P2} {P2} H {P3} |
1290 ---------------------------- |
1302 ---------------------------- |
1291 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1303 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1292 ------------------------------------------------ |
1304 ------------------------------------------------ |
1293 {P1} tcontra {P3} |
1305 {P1} tcontra {P3} |
1294 *) |
1306 *) |
1295 |
1307 |
1296 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1308 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1297 |
1309 |
1298 (* {P1} (tcopy |+| H) {P3} *) |
1310 (* {P1} (tcopy |+| H) {P3} *) |
1299 have first: "{P1} (tcopy |+| H) {P3}" |
1311 have first: "{P1} (tcopy |+| H) {P3}" |
1300 proof (induct rule: Hoare_plus_halt_simple) |
1312 proof (cases rule: Hoare_plus_halt_simple) |
1301 case A_halt (* of tcopy *) |
1313 case A_halt (* of tcopy *) |
1302 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1314 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1303 by (rule tcopy_correct1) (simp) |
1315 by (rule tcopy_correct1) (simp) |
1304 moreover |
1316 moreover |
1305 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1317 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1358 (* |
1370 (* |
1359 {P1} tcopy {P2} {P2} H {P3} |
1371 {P1} tcopy {P2} {P2} H {P3} |
1360 ---------------------------- |
1372 ---------------------------- |
1361 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1373 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1362 ------------------------------------------------ |
1374 ------------------------------------------------ |
1363 {P1} tcontra loops |
1375 {P1} tcontra loops |
1364 *) |
1376 *) |
1365 |
1377 |
1366 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1378 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1367 |
1379 |
1368 (* {P1} (tcopy |+| H) {P3} *) |
1380 (* {P1} (tcopy |+| H) {P3} *) |
1369 have first: "{P1} (tcopy |+| H) {P3}" |
1381 have first: "{P1} (tcopy |+| H) {P3}" |
1370 proof (induct rule: Hoare_plus_halt_simple) |
1382 proof (cases rule: Hoare_plus_halt_simple) |
1371 case A_halt (* of tcopy *) |
1383 case A_halt (* of tcopy *) |
1372 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1384 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1373 by (rule tcopy_correct1) (simp) |
1385 by (rule tcopy_correct1) (simp) |
1374 moreover |
1386 moreover |
1375 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1387 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |