1244 thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]" |
1248 thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]" |
1245 by(auto elim: tinres_ex1) |
1249 by(auto elim: tinres_ex1) |
1246 qed |
1250 qed |
1247 qed |
1251 qed |
1248 |
1252 |
1249 (* |
|
1250 lemma haltP_weaking: |
|
1251 "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow> |
|
1252 \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) |
|
1253 ((tcopy |+| H) |+| dither) stp)" |
|
1254 apply(simp add: haltP_def, auto) |
|
1255 apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def) |
|
1256 done |
|
1257 *) |
|
1258 |
|
1259 definition tcontra :: "instr list \<Rightarrow> instr list" |
1253 definition tcontra :: "instr list \<Rightarrow> instr list" |
1260 where |
1254 where |
1261 "tcontra h \<equiv> ((tcopy |+| h) |+| dither)" |
1255 "tcontra h \<equiv> (tcopy |+| h) |+| dither" |
1262 |
1256 |
1263 declare replicate_Suc[simp del] |
1257 declare replicate_Suc[simp del] |
1264 |
|
1265 lemma uh_h: "\<not> haltP (tcontra H, 0) [code (tcontra H)] |
|
1266 \<Longrightarrow> haltP (tcontra H, 0) [code (tcontra H)]" |
|
1267 proof(simp only: tcontra_def) |
|
1268 let ?tcontr = "(tcopy |+| H) |+| dither" |
|
1269 let ?cn = "Suc (code ?tcontr)" |
|
1270 let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))" |
|
1271 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
|
1272 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
|
1273 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
|
1274 let ?P3 = ?Q2 |
|
1275 let ?Q3 = ?P3 |
|
1276 assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]" |
|
1277 have "{?P1} ?tcontr {?Q3}" |
|
1278 proof(rule_tac Hoare_plus_halt, auto) |
|
1279 show "?Q2 \<mapsto> ?P3" |
|
1280 apply(simp add: assert_imp_def) |
|
1281 done |
|
1282 next |
|
1283 show "{?P1} (tcopy|+|H) {?Q2}" |
|
1284 proof(rule_tac Hoare_plus_halt, auto) |
|
1285 show "?Q1 \<mapsto> ?P2" |
|
1286 apply(simp add: assert_imp_def) |
|
1287 done |
|
1288 next |
|
1289 show "{?P1} tcopy {?Q1}" |
|
1290 proof - |
|
1291 have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}" |
|
1292 by(rule_tac tcopy_correct1, simp) |
|
1293 thus "?thesis" |
|
1294 proof(rule_tac Hoare_weak) |
|
1295 show "{inv_init1 ?cn} tcopy |
|
1296 {inv_end0 ?cn} " using g by simp |
|
1297 next |
|
1298 show "?P1 \<mapsto> inv_init1 (?cn)" |
|
1299 apply(simp add: inv_init1.simps assert_imp_def) |
|
1300 done |
|
1301 next |
|
1302 show "inv_end0 ?cn \<mapsto> ?Q1" |
|
1303 apply(simp add: assert_imp_def inv_end0.simps) |
|
1304 done |
|
1305 qed |
|
1306 qed |
|
1307 next |
|
1308 show "{?P2} H {?Q2}" |
|
1309 using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h |
|
1310 apply(auto) |
|
1311 apply(rule_tac x = na in exI) |
|
1312 apply(simp add: replicate_Suc tape_of_nl_abv) |
|
1313 done |
|
1314 qed |
|
1315 next |
|
1316 show "{?P3} dither {?Q3}" |
|
1317 using Hoare_def |
|
1318 proof(auto) |
|
1319 fix nd |
|
1320 show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and> |
|
1321 (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]) |
|
1322 holds_for steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n" |
|
1323 using dither_halt_rs[of nd] |
|
1324 apply(auto) |
|
1325 apply(rule_tac x = stp in exI, simp) |
|
1326 done |
|
1327 qed |
|
1328 qed |
|
1329 thus "False" |
|
1330 using h |
|
1331 apply(auto simp: haltP_def Hoare_def) |
|
1332 apply(erule_tac x = n in allE) |
|
1333 apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n") |
|
1334 apply(simp, auto) |
|
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) |
|
1337 apply(erule_tac x = 0 in allE, simp) |
|
1338 done |
|
1339 qed |
|
1340 |
|
1341 |
1258 |
1342 lemma dither_loops: |
1259 lemma dither_loops: |
1343 shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>" |
1260 shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>" |
1344 apply(rule Hoare_unhaltI) |
1261 apply(rule Hoare_unhaltI) |
1345 apply(auto intro!: dither_unhalt_rs) |
1262 apply(auto intro!: dither_unhalt_rs) |
1346 done |
1263 done |
1347 |
1264 |
1348 lemma h_uh: |
1265 lemma dither_halts: |
1349 assumes "haltP (tcontra H, 0) [code (tcontra H)]" |
1266 shows |
1350 shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]" |
1267 "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])} dither {(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])}" |
1351 proof - |
1268 apply(rule HoareI) |
1352 (* code of tcontra *) |
1269 using dither_halt_rs |
|
1270 apply(auto) |
|
1271 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases) |
|
1272 |
|
1273 lemma uh_h: |
|
1274 assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]" |
|
1275 shows "haltP0 (tcontra H) [code (tcontra H)]" |
|
1276 proof - |
|
1277 (* code of tcontra *) |
1353 def code_tcontra \<equiv> "(code (tcontra H))" |
1278 def code_tcontra \<equiv> "(code (tcontra H))" |
|
1279 have assms': "\<not> haltP0 (tcontra H) [code_tcontra]" |
|
1280 using assms by (simp add: code_tcontra_def) |
1354 |
1281 |
1355 (* invariants *) |
1282 (* invariants *) |
1356 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1283 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
1357 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1284 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
1358 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1285 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]" |
1359 |
1286 |
1360 (* |
1287 (* |
1361 {P1} tcopy {P2} {P2} H {P3} |
1288 {P1} tcopy {P2} {P2} H {P3} |
1362 ---------------------------- |
1289 ---------------------------- |
1363 {P1} (tcopy |+| H) {P3} {P3} dither loops |
1290 {P1} (tcopy |+| H) {P3} {P3} dither {P3} |
1364 ------------------------------------------------ |
1291 ------------------------------------------------ |
1365 {P1} (tcontra H) loops |
1292 {P1} (tcontra H) {P3} |
1366 *) |
1293 *) |
1367 |
1294 |
1368 have tm1_wf: "tm_wf0 tcopy" by auto |
1295 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
1369 have tm2_wf: "tm_wf0 (tcopy |+| H)" by auto |
|
1370 |
1296 |
1371 (* {P1} (tcopy |+| H) {P3} *) |
1297 (* {P1} (tcopy |+| H) {P3} *) |
1372 have first: "{P1} (tcopy |+| H) {P3}" |
1298 have first: "{P1} (tcopy |+| H) {P3}" |
1373 proof (induct rule: Hoare_plus_halt_simple) |
1299 proof (induct rule: Hoare_plus_halt_simple) |
1374 case A_halt (* of tcopy *) |
1300 case A_halt (* of tcopy *) |
1383 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) |
1384 ultimately |
1310 ultimately |
1385 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1311 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
1386 next |
1312 next |
1387 case B_halt |
1313 case B_halt |
1388 show "{P2} H {P3}" |
1314 obtain n i |
1389 using Hoare_def h_newcase[of "tcontra H" "[code_tcontra]" 1] assms |
1315 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])" |
1390 unfolding tcontra_def P2_def P3_def code_tcontra_def |
1316 using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def] |
|
1317 by (auto) |
|
1318 then show "{P2} H {P3}" |
|
1319 unfolding P2_def P3_def |
|
1320 unfolding Hoare_def |
1391 apply(auto) |
1321 apply(auto) |
1392 apply(rule_tac x = na in exI) |
1322 apply(rule_tac x = n in exI) |
1393 apply(simp add: replicate_Suc tape_of_nl_abv) |
1323 apply(simp add: replicate_Suc) |
1394 done |
1324 done |
1395 qed (simp add: tm1_wf) |
1325 qed (simp) |
|
1326 |
|
1327 (* {P3} dither {P3} *) |
|
1328 have second: "{P3} dither {P3}" unfolding P3_def |
|
1329 by (rule dither_halts) |
|
1330 |
|
1331 (* {P1} tcontra {P3} *) |
|
1332 have "{P1} (tcontra H) {P3}" unfolding tcontra_def |
|
1333 by (rule Hoare_plus_halt_simple[OF first second H_wf]) |
|
1334 |
|
1335 with assms' have "False" |
|
1336 unfolding P1_def P3_def code_tcontra_def |
|
1337 unfolding haltP_def |
|
1338 unfolding Hoare_def |
|
1339 apply(auto) |
|
1340 apply(erule_tac x = n in allE) |
|
1341 apply(case_tac "steps0 (Suc 0, [], <[code (tcontra H)]>) (tcontra H) n") |
|
1342 apply(simp, auto) |
|
1343 apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE) |
|
1344 apply(simp) |
|
1345 by (smt replicate_0 replicate_Suc) |
|
1346 then show "haltP0 (tcontra H) [code (tcontra H)]" |
|
1347 by blast |
|
1348 qed |
|
1349 |
|
1350 lemma h_uh: |
|
1351 assumes "haltP0 (tcontra H) [code (tcontra H)]" |
|
1352 shows "\<not> haltP0 (tcontra H) [code (tcontra H)]" |
|
1353 proof - |
|
1354 (* code of tcontra *) |
|
1355 def code_tcontra \<equiv> "(code (tcontra H))" |
|
1356 have assms': "haltP0 (tcontra H) [code_tcontra]" |
|
1357 using assms by (simp add: code_tcontra_def) |
|
1358 |
|
1359 (* invariants *) |
|
1360 def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)" |
|
1361 def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)" |
|
1362 def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
|
1363 |
|
1364 (* |
|
1365 {P1} tcopy {P2} {P2} H {P3} |
|
1366 ---------------------------- |
|
1367 {P1} (tcopy |+| H) {P3} {P3} dither loops |
|
1368 ------------------------------------------------ |
|
1369 {P1} (tcontra H) loops |
|
1370 *) |
|
1371 |
|
1372 have H_wf: "tm_wf0 (tcopy |+| H)" by auto |
|
1373 |
|
1374 (* {P1} (tcopy |+| H) {P3} *) |
|
1375 have first: "{P1} (tcopy |+| H) {P3}" |
|
1376 proof (induct rule: Hoare_plus_halt_simple) |
|
1377 case A_halt (* of tcopy *) |
|
1378 have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}" |
|
1379 unfolding code_tcontra_def |
|
1380 by (rule tcopy_correct1) (simp) |
|
1381 moreover |
|
1382 have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def |
|
1383 by (simp add: assert_imp_def tape_of_nl_abv) |
|
1384 moreover |
|
1385 have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def |
|
1386 by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv) |
|
1387 ultimately |
|
1388 show "{P1} tcopy {P2}" by (rule Hoare_weak) |
|
1389 next |
|
1390 case B_halt |
|
1391 obtain n i |
|
1392 where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])" |
|
1393 using h_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def] |
|
1394 by (auto) |
|
1395 then show "{P2} H {P3}" |
|
1396 unfolding P2_def P3_def |
|
1397 unfolding Hoare_def |
|
1398 apply(auto) |
|
1399 apply(rule_tac x = n in exI) |
|
1400 apply(simp add: replicate_Suc) |
|
1401 done |
|
1402 qed (simp) |
1396 |
1403 |
1397 (* {P3} dither loops *) |
1404 (* {P3} dither loops *) |
1398 have second: "{P3} dither \<up>" unfolding P3_def |
1405 have second: "{P3} dither \<up>" unfolding P3_def |
1399 by (rule dither_loops) |
1406 by (rule dither_loops) |
1400 |
1407 |
1401 (* {P1} tcontra loops *) |
1408 (* {P1} tcontra loops *) |
1402 have "{P1} (tcontra H) \<up>" unfolding tcontra_def |
1409 have "{P1} (tcontra H) \<up>" unfolding tcontra_def |
1403 by (rule Hoare_plus_unhalt_simple[OF first second tm2_wf]) |
1410 by (rule Hoare_plus_unhalt_simple[OF first second H_wf]) |
1404 |
1411 |
1405 then show "\<not> haltP (tcontra H, 0) [code_tcontra]" |
1412 with assms have "False" |
1406 using assms |
1413 unfolding haltP_def |
1407 unfolding tcontra_def code_tcontra_def |
1414 unfolding P1_def code_tcontra_def |
1408 apply(auto simp: haltP_def Hoare_unhalt_def P1_def) |
1415 unfolding Hoare_unhalt_def |
1409 apply(erule_tac x = n in allE) |
1416 by (auto, metis is_final_eq) |
1410 apply(case_tac "steps (Suc 0, [], <[code ((tcopy |+| H) |+| dither)]>) (tcontra H, 0) n") |
1417 then show "\<not> haltP0 (tcontra H) [code_tcontra]" |
1411 apply(simp add: tape_of_nl_abv tcontra_def code_tcontra_def tape_of_nat_abv) |
1418 by blast |
1412 done |
|
1413 qed |
1419 qed |
1414 |
1420 |
1415 |
1421 |
1416 |
1422 |
1417 |
1423 |