1335 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) |
1336 apply(simp add: numeral replicate_Suc tape_of_nl_abv) |
1336 apply(simp add: numeral replicate_Suc tape_of_nl_abv) |
1337 apply(erule_tac x = 0 in allE, simp) |
1337 apply(erule_tac x = 0 in allE, simp) |
1338 done |
1338 done |
1339 qed |
1339 qed |
|
1340 |
|
1341 |
|
1342 lemma dither_loops: |
|
1343 shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>" |
|
1344 apply(rule Hoare_unhaltI) |
|
1345 apply(auto intro!: dither_unhalt_rs) |
|
1346 done |
1340 |
1347 |
1341 |
|
1342 |
|
1343 |
|
1344 lemma h_uh: |
1348 lemma h_uh: |
1345 assumes "haltP (tcontra H, 0) [code (tcontra H)]" |
1349 assumes "haltP (tcontra H, 0) [code (tcontra H)]" |
1346 shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]" |
1350 shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]" |
1347 proof(simp only: tcontra_def) |
1351 proof - |
1348 let ?tcontr = "(tcopy |+| H) |+| dither" |
1352 (* code of tcontra *) |
1349 let ?cn = "Suc (code ?tcontr)" |
1353 def code_tcontra \<equiv> "(code (tcontra H))" |
1350 let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))" |
1354 |
1351 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1355 (* invariants *) |
1352 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1356 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1353 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1357 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1354 let ?P3 = ?Q2 |
1358 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1355 have "{?P1} ?tcontr \<up>" |
1359 |
1356 proof(rule_tac Hoare_plus_unhalt, auto) |
1360 (* |
1357 show "?Q2 \<mapsto> ?P3" |
1361 {P1} tcopy {P2} {P2} H {P3} |
1358 apply(simp add: assert_imp_def) |
1362 ---------------------------- |
|
1363 {P1} (tcopy |+| H) {P3} {P3} dither loops |
|
1364 ------------------------------------------------ |
|
1365 {P1} (tcontra H) loops |
|
1366 *) |
|
1367 |
|
1368 have tm1_wf: "tm_wf0 tcopy" by auto |
|
1369 have tm2_wf: "tm_wf0 (tcopy |+| H)" by auto |
|
1370 |
|
1371 (* {P1} (tcopy |+| H) {P3} *) |
|
1372 have first: "{P1} (tcopy |+| H) {P3}" |
|
1373 proof (induct rule: Hoare_plus_halt_simple) |
|
1374 case A_halt (* of tcopy *) |
|
1375 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
|
1376 unfolding code_tcontra_def |
|
1377 by (rule tcopy_correct1) (simp) |
|
1378 moreover |
|
1379 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
|
1380 by (simp add: assert_imp_def tape_of_nl_abv) |
|
1381 moreover |
|
1382 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def |
|
1383 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
|
1384 ultimately |
|
1385 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
|
1386 next |
|
1387 case B_halt |
|
1388 show "{P2} H {P3}" |
|
1389 using Hoare_def h_newcase[of "tcontra H" "[code_tcontra]" 1] assms |
|
1390 unfolding tcontra_def P2_def P3_def code_tcontra_def |
|
1391 apply(auto) |
|
1392 apply(rule_tac x = na in exI) |
|
1393 apply(simp add: replicate_Suc tape_of_nl_abv) |
1359 done |
1394 done |
1360 next |
1395 qed (simp add: tm1_wf) |
1361 show "{?P1} (tcopy |+| H) {?Q2}" |
1396 |
1362 proof(rule_tac Hoare_plus_halt, auto) |
1397 (* {P3} dither loops *) |
1363 show "?Q1 \<mapsto> ?P2" |
1398 have second: "{P3} dither \<up>" unfolding P3_def |
1364 apply(simp add: assert_imp_def) |
1399 by (rule dither_loops) |
1365 done |
1400 |
1366 next |
1401 (* {P1} tcontra loops *) |
1367 show "{?P1} tcopy {?Q1}" |
1402 have "{P1} (tcontra H) \<up>" unfolding tcontra_def |
1368 proof - |
1403 by (rule Hoare_plus_unhalt_simple[OF first second tm2_wf]) |
1369 have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}" |
1404 |
1370 by(rule_tac tcopy_correct1, simp) |
1405 then show "\<not> haltP (tcontra H, 0) [code_tcontra]" |
1371 thus "?thesis" |
|
1372 proof(rule_tac Hoare_weak) |
|
1373 show "{inv_init1 ?cn} tcopy |
|
1374 {inv_end0 ?cn} " using g by simp |
|
1375 next |
|
1376 show "?P1 \<mapsto> inv_init1 (?cn)" |
|
1377 apply(simp add: inv_init1.simps assert_imp_def) |
|
1378 done |
|
1379 next |
|
1380 show "inv_end0 ?cn \<mapsto> ?Q1" |
|
1381 apply(simp add: assert_imp_def inv_end0.simps) |
|
1382 done |
|
1383 qed |
|
1384 qed |
|
1385 next |
|
1386 show "{?P2} H {?Q2}" |
|
1387 using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] assms |
|
1388 unfolding tcontra_def |
|
1389 apply(auto) |
|
1390 apply(rule_tac x = na in exI) |
|
1391 apply(simp add: replicate_Suc tape_of_nl_abv) |
|
1392 done |
|
1393 qed |
|
1394 next |
|
1395 show "{?P3} dither \<up>" |
|
1396 using Hoare_unhalt_def |
|
1397 proof(auto) |
|
1398 fix nd n |
|
1399 assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" |
|
1400 thus "False" |
|
1401 using dither_unhalt_rs[of nd n] |
|
1402 by simp |
|
1403 qed |
|
1404 qed |
|
1405 thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]" |
|
1406 using assms |
1406 using assms |
1407 unfolding tcontra_def |
1407 unfolding tcontra_def code_tcontra_def |
1408 apply(auto simp: haltP_def Hoare_unhalt_def) |
1408 apply(auto simp: haltP_def Hoare_unhalt_def P1_def) |
1409 apply(erule_tac x = n in allE) |
1409 apply(erule_tac x = n in allE) |
1410 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
1410 apply(case_tac "steps (Suc 0, [], <[code ((tcopy |+| H) |+| dither)]>) (tcontra H, 0) n") |
1411 apply(simp add: tape_of_nl_abv) |
1411 apply(simp add: tape_of_nl_abv tcontra_def code_tcontra_def tape_of_nat_abv) |
1412 done |
1412 done |
1413 qed |
1413 qed |
1414 |
1414 |
|
1415 |
|
1416 |
1415 |
1417 |
1416 text {* |
1418 text {* |
1417 @{text "False"} is finally derived. |
1419 @{text "False"} can finally derived. |
1418 *} |
1420 *} |
1419 |
1421 |
1420 lemma false: "False" |
1422 lemma false: "False" |
1421 using uh_h h_uh |
1423 using uh_h h_uh |
1422 by auto |
1424 by auto |