990 apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp |
987 apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp |
991 tm_comp.simps) |
988 tm_comp.simps) |
992 done |
989 done |
993 |
990 |
994 lemma tcopy_correct1: |
991 lemma tcopy_correct1: |
995 "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} (tcopy, 0) {inv_end0 x}" |
992 "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}" |
996 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt) |
993 proof(simp add: tcopy_def, rule_tac Hoare_plus_halt) |
997 show "inv_loop0 x \<mapsto> inv_end1 x" |
994 show "inv_loop0 x \<mapsto> inv_end1 x" |
998 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def) |
995 by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def) |
999 next |
996 next |
1000 show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto |
997 show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto |
1001 next |
998 next |
1002 show "tm_wf (tcopy_end, 0)" by auto |
999 show "tm_wf (tcopy_end, 0)" by auto |
1003 next |
1000 next |
1004 assume "0 < x" |
1001 assume "0 < x" |
1005 thus "{inv_init1 x} (tcopy_init |+| tcopy_loop, 0) {inv_loop0 x}" |
1002 thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}" |
1006 proof(rule_tac Hoare_plus_halt) |
1003 proof(rule_tac Hoare_plus_halt) |
1007 show "inv_init0 x \<mapsto> inv_loop1 x" |
1004 show "inv_init0 x \<mapsto> inv_loop1 x" |
1008 apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def) |
1005 apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def) |
1009 apply(rule_tac x = "Suc 0" in exI, auto) |
1006 apply(rule_tac x = "Suc 0" in exI, auto) |
1010 done |
1007 done |
1012 show "tm_wf (tcopy_init, 0)" by auto |
1009 show "tm_wf (tcopy_init, 0)" by auto |
1013 next |
1010 next |
1014 show "tm_wf (tcopy_loop, 0)" by auto |
1011 show "tm_wf (tcopy_loop, 0)" by auto |
1015 next |
1012 next |
1016 assume "0 < x" |
1013 assume "0 < x" |
1017 thus "{inv_init1 x} (tcopy_init, 0) {inv_init0 x}" |
1014 thus "{inv_init1 x} tcopy_init {inv_init0 x}" |
1018 by(erule_tac init_correct) |
1015 by(erule_tac init_correct) |
1019 next |
1016 next |
1020 assume "0 < x" |
1017 assume "0 < x" |
1021 thus "{inv_loop1 x} (tcopy_loop, 0) {inv_loop0 x}" |
1018 thus "{inv_loop1 x} tcopy_loop {inv_loop0 x}" |
1022 by(erule_tac loop_correct) |
1019 by(erule_tac loop_correct) |
1023 qed |
1020 qed |
1024 next |
1021 next |
1025 assume "0 < x" |
1022 assume "0 < x" |
1026 thus "{inv_end1 x} (tcopy_end, 0) {inv_end0 x}" |
1023 thus "{inv_end1 x} tcopy_end {inv_end0 x}" |
1027 by(erule_tac end_correct) |
1024 by(erule_tac end_correct) |
1028 qed |
1025 qed |
1029 |
1026 |
1030 section {* |
1027 section {* |
1031 The {\em Dithering} Turing Machine |
1028 The {\em Dithering} Turing Machine |
1145 apply arith |
1142 apply arith |
1146 apply(drule_tac length_eq, simp) |
1143 apply(drule_tac length_eq, simp) |
1147 done |
1144 done |
1148 |
1145 |
1149 lemma Hoare_weak: |
1146 lemma Hoare_weak: |
1150 "\<lbrakk>{P} (p, off) {Q}; P'\<mapsto>P; Q\<mapsto>Q'\<rbrakk> \<Longrightarrow> {P'} (p, off) {Q'}" |
1147 fixes p::tprog0 |
1151 using Hoare_def |
1148 assumes a: "{P} p {Q}" |
1152 proof(auto simp: assert_imp_def) |
1149 and b: "P' \<mapsto> P" |
1153 fix l r |
1150 and c: "Q \<mapsto> Q'" |
1154 assume |
1151 shows "{P'} p {Q'}" |
1155 ho1: "\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) |
1152 using assms |
1156 \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)" |
1153 unfolding Hoare_def assert_imp_def |
1157 and imp1: "\<forall>l r. P' (l, r) \<longrightarrow> P (l, r)" |
1154 by (blast intro: holds_for_imp[simplified assert_imp_def]) |
1158 and imp2: "\<forall>l r. Q (l, r) \<longrightarrow> Q' (l, r)" |
|
1159 and cond: "P' (l, r)" |
|
1160 and ho2: "\<And>P a b Q. {P} (a, b) {Q} \<equiv> \<forall>l r. P (l, r) \<longrightarrow> |
|
1161 (\<exists>n. is_final (steps (Suc 0, l, r) (a, b) n) \<and> Q holds_for steps (Suc 0, l, r) (a, b) n)" |
|
1162 have "P (l, r)" |
|
1163 using cond imp1 by auto |
|
1164 hence "(\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) |
|
1165 \<and> Q holds_for steps (Suc 0, l, r) (p, off) n)" |
|
1166 using ho1 by auto |
|
1167 from this obtain n where "is_final (steps (Suc 0, l, r) (p, off) n) |
|
1168 \<and> Q holds_for steps (Suc 0, l, r) (p, off) n" .. |
|
1169 thus "\<exists>n. is_final (steps (Suc 0, l, r) (p, off) n) \<and> |
|
1170 Q' holds_for steps (Suc 0, l, r) (p, off) n" |
|
1171 apply(rule_tac x = n in exI, auto) |
|
1172 apply(case_tac "steps (Suc 0, l, r) (p, off) n", simp) |
|
1173 using imp2 |
|
1174 by simp |
|
1175 qed |
|
1176 |
1155 |
1177 text {* |
1156 text {* |
1178 The following locale specifies that TM @{text "H"} can be used to solve |
1157 The following locale specifies that TM @{text "H"} can be used to solve |
1179 the {\em Halting Problem} and @{text "False"} is going to be derived |
1158 the {\em Halting Problem} and @{text "False"} is going to be derived |
1180 under this locale. Therefore, the undecidability of {\em Halting Problem} |
1159 under this locale. Therefore, the undecidability of {\em Halting Problem} |
1297 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1276 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1298 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
1277 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
1299 let ?P3 = ?Q2 |
1278 let ?P3 = ?Q2 |
1300 let ?Q3 = ?P3 |
1279 let ?Q3 = ?P3 |
1301 assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]" |
1280 assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]" |
1302 have "{?P1} (?tcontr, 0) {?Q3}" |
1281 have "{?P1} ?tcontr {?Q3}" |
1303 proof(rule_tac Hoare_plus_halt, auto) |
1282 proof(rule_tac Hoare_plus_halt, auto) |
1304 show "?Q2 \<mapsto> ?P3" |
1283 show "?Q2 \<mapsto> ?P3" |
1305 apply(simp add: assert_imp_def) |
1284 apply(simp add: assert_imp_def) |
1306 done |
1285 done |
1307 next |
1286 next |
1308 show "{?P1} (tcopy|+|H, 0) {?Q2}" |
1287 show "{?P1} (tcopy|+|H) {?Q2}" |
1309 proof(rule_tac Hoare_plus_halt, auto) |
1288 proof(rule_tac Hoare_plus_halt, auto) |
1310 show "?Q1 \<mapsto> ?P2" |
1289 show "?Q1 \<mapsto> ?P2" |
1311 apply(simp add: assert_imp_def) |
1290 apply(simp add: assert_imp_def) |
1312 done |
1291 done |
1313 next |
1292 next |
1314 show "{?P1} (tcopy, 0) {?Q1}" |
1293 show "{?P1} tcopy {?Q1}" |
1315 proof - |
1294 proof - |
1316 have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}" |
1295 have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}" |
1317 by(rule_tac tcopy_correct1, simp) |
1296 by(rule_tac tcopy_correct1, simp) |
1318 thus "?thesis" |
1297 thus "?thesis" |
1319 proof(rule_tac Hoare_weak) |
1298 proof(rule_tac Hoare_weak) |
1320 show "{inv_init1 ?cn} (tcopy, 0) |
1299 show "{inv_init1 ?cn} tcopy |
1321 {inv_end0 ?cn} " using g by simp |
1300 {inv_end0 ?cn} " using g by simp |
1322 next |
1301 next |
1323 show "?P1 \<mapsto> inv_init1 (?cn)" |
1302 show "?P1 \<mapsto> inv_init1 (?cn)" |
1324 apply(simp add: inv_init1.simps assert_imp_def) |
1303 apply(simp add: inv_init1.simps assert_imp_def) |
1325 done |
1304 done |
1328 apply(simp add: assert_imp_def inv_end0.simps) |
1307 apply(simp add: assert_imp_def inv_end0.simps) |
1329 done |
1308 done |
1330 qed |
1309 qed |
1331 qed |
1310 qed |
1332 next |
1311 next |
1333 show "{?P2} (H, 0) {?Q2}" |
1312 show "{?P2} H {?Q2}" |
1334 using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1313 using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1335 apply(auto) |
1314 apply(auto) |
1336 apply(rule_tac x = na in exI) |
1315 apply(rule_tac x = na in exI) |
1337 apply(simp add: replicate_Suc tape_of_nl_abv) |
1316 apply(simp add: replicate_Suc tape_of_nl_abv) |
1338 done |
1317 done |
1339 qed |
1318 qed |
1340 next |
1319 next |
1341 show "{?P3}(dither, 0){?Q3}" |
1320 show "{?P3} dither {?Q3}" |
1342 using Hoare_def |
1321 using Hoare_def |
1343 proof(auto) |
1322 proof(auto) |
1344 fix nd |
1323 fix nd |
1345 show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and> |
1324 show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and> |
1346 (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]) |
1325 (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]) |
1373 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1352 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1374 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1353 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1375 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1354 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1376 let ?P3 = ?Q2 |
1355 let ?P3 = ?Q2 |
1377 assume h: "haltP (?tcontr, 0) [code ?tcontr]" |
1356 assume h: "haltP (?tcontr, 0) [code ?tcontr]" |
1378 have "{?P1} (?tcontr, 0)" |
1357 have "{?P1} ?tcontr" |
1379 proof(rule_tac Hoare_plus_unhalt, auto) |
1358 proof(rule_tac Hoare_plus_unhalt, auto) |
1380 show "?Q2 \<mapsto> ?P3" |
1359 show "?Q2 \<mapsto> ?P3" |
1381 apply(simp add: assert_imp_def) |
1360 apply(simp add: assert_imp_def) |
1382 done |
1361 done |
1383 next |
1362 next |
1384 show "{?P1} (tcopy|+|H, 0) {?Q2}" |
1363 show "{?P1} (tcopy |+| H) {?Q2}" |
1385 proof(rule_tac Hoare_plus_halt, auto) |
1364 proof(rule_tac Hoare_plus_halt, auto) |
1386 show "?Q1 \<mapsto> ?P2" |
1365 show "?Q1 \<mapsto> ?P2" |
1387 apply(simp add: assert_imp_def) |
1366 apply(simp add: assert_imp_def) |
1388 done |
1367 done |
1389 next |
1368 next |
1390 show "{?P1} (tcopy, 0) {?Q1}" |
1369 show "{?P1} tcopy {?Q1}" |
1391 proof - |
1370 proof - |
1392 have g: "{inv_init1 ?cn} (tcopy, 0) {inv_end0 ?cn}" |
1371 have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}" |
1393 by(rule_tac tcopy_correct1, simp) |
1372 by(rule_tac tcopy_correct1, simp) |
1394 thus "?thesis" |
1373 thus "?thesis" |
1395 proof(rule_tac Hoare_weak) |
1374 proof(rule_tac Hoare_weak) |
1396 show "{inv_init1 ?cn} (tcopy, 0) |
1375 show "{inv_init1 ?cn} tcopy |
1397 {inv_end0 ?cn} " using g by simp |
1376 {inv_end0 ?cn} " using g by simp |
1398 next |
1377 next |
1399 show "?P1 \<mapsto> inv_init1 (?cn)" |
1378 show "?P1 \<mapsto> inv_init1 (?cn)" |
1400 apply(simp add: inv_init1.simps assert_imp_def) |
1379 apply(simp add: inv_init1.simps assert_imp_def) |
1401 done |
1380 done |
1404 apply(simp add: assert_imp_def inv_end0.simps) |
1383 apply(simp add: assert_imp_def inv_end0.simps) |
1405 done |
1384 done |
1406 qed |
1385 qed |
1407 qed |
1386 qed |
1408 next |
1387 next |
1409 show "{?P2} (H, 0) {?Q2}" |
1388 show "{?P2} H {?Q2}" |
1410 using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1389 using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h |
1411 apply(auto) |
1390 apply(auto) |
1412 apply(rule_tac x = na in exI) |
1391 apply(rule_tac x = na in exI) |
1413 apply(simp add: replicate_Suc tape_of_nl_abv) |
1392 apply(simp add: replicate_Suc tape_of_nl_abv) |
1414 done |
1393 done |
1415 qed |
1394 qed |
1416 next |
1395 next |
1417 show "{?P3}(dither, 0)" |
1396 show "{?P3} dither" |
1418 using Hoare_unhalt_def |
1397 using Hoare_unhalt_def |
1419 proof(auto) |
1398 proof(auto) |
1420 fix nd n |
1399 fix nd n |
1421 assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" |
1400 assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" |
1422 thus "False" |
1401 thus "False" |