1267 thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]" |
1267 thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]" |
1268 by(auto elim: tinres_ex1) |
1268 by(auto elim: tinres_ex1) |
1269 qed |
1269 qed |
1270 qed |
1270 qed |
1271 |
1271 |
1272 (* TM that produces the contradiction *) |
1272 (* TM that produces the contradiction and its code *) |
1273 definition tcontra :: "instr list \<Rightarrow> instr list" |
1273 abbreviation |
1274 where |
1274 "tcontra \<equiv> (tcopy |+| H) |+| dither" |
1275 "tcontra h \<equiv> (tcopy |+| h) |+| dither" |
1275 abbreviation |
1276 |
1276 "code_tcontra \<equiv> code tcontra" |
1277 |
1277 |
1278 lemma uh_h: |
1278 (* assume tcontra does not halt on its code *) |
1279 assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]" |
1279 lemma tcontra_unhalt: |
|
1280 assumes "\<not> haltP0 tcontra [code tcontra]" |
1280 shows "False" |
1281 shows "False" |
1281 proof - |
1282 proof - |
1282 (* code of tcontra *) |
|
1283 def code_tcontra \<equiv> "(code (tcontra H))" |
|
1284 have assms': "\<not> haltP0 (tcontra H) [code_tcontra]" |
|
1285 using assms by (simp add: code_tcontra_def) |
|
1286 |
|
1287 (* invariants *) |
1283 (* invariants *) |
1288 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1284 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1289 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1285 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1290 def P3 \<equiv> dither_halt_inv |
1286 def P3 \<equiv> dither_halt_inv |
1291 |
1287 |
1292 (* |
1288 (* |
1293 {P1} tcopy {P2} {P2} H {P3} |
1289 {P1} tcopy {P2} {P2} H {P3} |
1294 ---------------------------- |
1290 ---------------------------- |
1295 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1291 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1296 ------------------------------------------------ |
1292 ------------------------------------------------ |
1297 {P1} (tcontra H) {P3} |
1293 {P1} tcontra {P3} |
1298 *) |
1294 *) |
1299 |
1295 |
1300 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1296 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1301 |
1297 |
1302 (* {P1} (tcopy |+| H) {P3} *) |
1298 (* {P1} (tcopy |+| H) {P3} *) |
1303 have first: "{P1} (tcopy |+| H) {P3}" |
1299 have first: "{P1} (tcopy |+| H) {P3}" |
1304 proof (induct rule: Hoare_plus_halt_simple) |
1300 proof (induct rule: Hoare_plus_halt_simple) |
1305 case A_halt (* of tcopy *) |
1301 case A_halt (* of tcopy *) |
1306 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1302 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1307 unfolding code_tcontra_def |
|
1308 by (rule tcopy_correct1) (simp) |
1303 by (rule tcopy_correct1) (simp) |
1309 moreover |
1304 moreover |
1310 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1305 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1311 by (simp add: assert_imp_def tape_of_nl_abv) |
1306 by (simp add: assert_imp_def tape_of_nl_abv) |
1312 moreover |
1307 moreover |
1313 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def |
1308 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def |
1314 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
1309 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
1315 ultimately |
1310 ultimately |
1316 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1311 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1317 next |
1312 next |
1318 case B_halt |
1313 case B_halt |
1319 obtain n i |
1314 obtain n i |
1320 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])" |
1315 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])" |
1321 using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def] |
1316 using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |
1322 by (auto) |
1317 by (auto) |
1323 then show "{P2} H {P3}" |
1318 then show "{P2} H {P3}" |
1324 unfolding P2_def P3_def dither_halt_inv_def |
1319 unfolding P2_def P3_def dither_halt_inv_def |
1325 unfolding Hoare_def |
1320 unfolding Hoare_def |
1326 apply(auto) |
1321 apply(auto) |
1332 (* {P3} dither {P3} *) |
1327 (* {P3} dither {P3} *) |
1333 have second: "{P3} dither {P3}" unfolding P3_def |
1328 have second: "{P3} dither {P3}" unfolding P3_def |
1334 by (rule dither_halts) |
1329 by (rule dither_halts) |
1335 |
1330 |
1336 (* {P1} tcontra {P3} *) |
1331 (* {P1} tcontra {P3} *) |
1337 have "{P1} (tcontra H) {P3}" unfolding tcontra_def |
1332 have "{P1} tcontra {P3}" |
1338 by (rule Hoare_plus_halt_simple[OF first second H_wf]) |
1333 by (rule Hoare_plus_halt_simple[OF first second H_wf]) |
1339 |
1334 |
1340 with assms' show "False" |
1335 with assms show "False" |
1341 unfolding P1_def P3_def dither_halt_inv_def code_tcontra_def |
1336 unfolding P1_def P3_def dither_halt_inv_def |
1342 unfolding haltP_def |
1337 unfolding haltP_def |
1343 unfolding Hoare_def |
1338 unfolding Hoare_def |
1344 apply(auto) |
1339 apply(auto) |
1345 apply(erule_tac x = n in allE) |
1340 apply(erule_tac x = n in allE) |
1346 apply(case_tac "steps0 (Suc 0, [], <[code (tcontra H)]>) (tcontra H) n") |
1341 apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n") |
1347 apply(simp, auto) |
1342 apply(simp, auto) |
1348 apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE) |
1343 apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE) |
1349 apply(simp) |
1344 apply(simp) |
1350 by (smt replicate_0 replicate_Suc) |
1345 by (smt replicate_0 replicate_Suc) |
1351 qed |
1346 qed |
1352 |
1347 |
1353 lemma h_uh: |
1348 (* asumme tcontra halts on its code *) |
1354 assumes "haltP0 (tcontra H) [code (tcontra H)]" |
1349 lemma tcontra_halt: |
|
1350 assumes "haltP0 tcontra [code tcontra]" |
1355 shows "False" |
1351 shows "False" |
1356 proof - |
1352 proof - |
1357 (* code of tcontra *) |
|
1358 def code_tcontra \<equiv> "(code (tcontra H))" |
|
1359 have assms': "haltP0 (tcontra H) [code_tcontra]" |
|
1360 using assms by (simp add: code_tcontra_def) |
|
1361 |
|
1362 (* invariants *) |
1353 (* invariants *) |
1363 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1354 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1364 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1355 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1365 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1356 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1366 |
1357 |
1367 (* |
1358 (* |
1368 {P1} tcopy {P2} {P2} H {P3} |
1359 {P1} tcopy {P2} {P2} H {P3} |
1369 ---------------------------- |
1360 ---------------------------- |
1370 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1361 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1371 ------------------------------------------------ |
1362 ------------------------------------------------ |
1372 {P1} (tcontra H) loops |
1363 {P1} tcontra loops |
1373 *) |
1364 *) |
1374 |
1365 |
1375 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1366 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1376 |
1367 |
1377 (* {P1} (tcopy |+| H) {P3} *) |
1368 (* {P1} (tcopy |+| H) {P3} *) |
1378 have first: "{P1} (tcopy |+| H) {P3}" |
1369 have first: "{P1} (tcopy |+| H) {P3}" |
1379 proof (induct rule: Hoare_plus_halt_simple) |
1370 proof (induct rule: Hoare_plus_halt_simple) |
1380 case A_halt (* of tcopy *) |
1371 case A_halt (* of tcopy *) |
1381 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1372 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
1382 unfolding code_tcontra_def |
|
1383 by (rule tcopy_correct1) (simp) |
1373 by (rule tcopy_correct1) (simp) |
1384 moreover |
1374 moreover |
1385 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1375 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
1386 by (simp add: assert_imp_def tape_of_nl_abv) |
1376 by (simp add: assert_imp_def tape_of_nl_abv) |
1387 moreover |
1377 moreover |
1388 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def |
1378 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def |
1389 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
1379 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
1390 ultimately |
1380 ultimately |
1391 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1381 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1392 next |
1382 next |
1393 case B_halt |
1383 case B_halt |
1394 obtain n i |
1384 obtain n i |
1395 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])" |
1385 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])" |
1396 using h_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def] |
1386 using h_newcase[of "tcontra" "[code_tcontra]" 1, OF assms] |
1397 by (auto) |
1387 by (auto) |
1398 then show "{P2} H {P3}" |
1388 then show "{P2} H {P3}" |
1399 unfolding P2_def P3_def |
1389 unfolding P2_def P3_def |
1400 unfolding Hoare_def |
1390 unfolding Hoare_def |
1401 apply(auto) |
1391 apply(auto) |
1407 (* {P3} dither loops *) |
1397 (* {P3} dither loops *) |
1408 have second: "{P3} dither \<up>" unfolding P3_def |
1398 have second: "{P3} dither \<up>" unfolding P3_def |
1409 by (rule dither_loops) |
1399 by (rule dither_loops) |
1410 |
1400 |
1411 (* {P1} tcontra loops *) |
1401 (* {P1} tcontra loops *) |
1412 have "{P1} (tcontra H) \<up>" unfolding tcontra_def |
1402 have "{P1} tcontra \<up>" |
1413 by (rule Hoare_plus_unhalt_simple[OF first second H_wf]) |
1403 by (rule Hoare_plus_unhalt_simple[OF first second H_wf]) |
1414 |
1404 |
1415 with assms show "False" |
1405 with assms show "False" |
1416 unfolding haltP_def |
1406 unfolding haltP_def |
1417 unfolding P1_def code_tcontra_def |
1407 unfolding P1_def |
1418 unfolding Hoare_unhalt_def |
1408 unfolding Hoare_unhalt_def |
1419 by (auto, metis is_final_eq) |
1409 by (auto, metis is_final_eq) |
1420 qed |
1410 qed |
1421 |
|
1422 |
|
1423 |
|
1424 |
1411 |
1425 text {* |
1412 text {* |
1426 @{text "False"} can finally derived. |
1413 @{text "False"} can finally derived. |
1427 *} |
1414 *} |
1428 |
1415 |
1429 lemma false: "False" |
1416 lemma false: "False" |
1430 using uh_h h_uh by auto |
1417 using tcontra_halt tcontra_unhalt |
|
1418 by auto |
1431 |
1419 |
1432 end |
1420 end |
1433 |
1421 |
1434 declare replicate_Suc[simp del] |
1422 declare replicate_Suc[simp del] |
1435 |
1423 |