994 show "inv_loop0 x \<mapsto> inv_end1 x" |
994 show "inv_loop0 x \<mapsto> inv_end1 x" |
995 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) |
996 next |
996 next |
997 show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto |
997 show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto |
998 next |
998 next |
999 show "tm_wf (tcopy_end, 0)" by auto |
|
1000 next |
|
1001 assume "0 < x" |
999 assume "0 < x" |
1002 thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}" |
1000 thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}" |
1003 proof(rule_tac Hoare_plus_halt) |
1001 proof(rule_tac Hoare_plus_halt) |
1004 show "inv_init0 x \<mapsto> inv_loop1 x" |
1002 show "inv_init0 x \<mapsto> inv_loop1 x" |
1005 apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def) |
1003 apply(auto simp: inv_init0.simps inv_loop1.simps assert_imp_def) |
1006 apply(rule_tac x = "Suc 0" in exI, auto) |
1004 apply(rule_tac x = "Suc 0" in exI, auto) |
1007 done |
1005 done |
1008 next |
1006 next |
1009 show "tm_wf (tcopy_init, 0)" by auto |
1007 show "tm_wf (tcopy_init, 0)" by auto |
1010 next |
|
1011 show "tm_wf (tcopy_loop, 0)" by auto |
|
1012 next |
1008 next |
1013 assume "0 < x" |
1009 assume "0 < x" |
1014 thus "{inv_init1 x} tcopy_init {inv_init0 x}" |
1010 thus "{inv_init1 x} tcopy_init {inv_init0 x}" |
1015 by(erule_tac init_correct) |
1011 by(erule_tac init_correct) |
1016 next |
1012 next |
1343 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1339 let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1344 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1340 let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)" |
1345 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1341 let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]" |
1346 let ?P3 = ?Q2 |
1342 let ?P3 = ?Q2 |
1347 assume h: "haltP (?tcontr, 0) [code ?tcontr]" |
1343 assume h: "haltP (?tcontr, 0) [code ?tcontr]" |
1348 have "{?P1} ?tcontr" |
1344 have "{?P1} ?tcontr \<up>" |
1349 proof(rule_tac Hoare_plus_unhalt, auto) |
1345 proof(rule_tac Hoare_plus_unhalt, auto) |
1350 show "?Q2 \<mapsto> ?P3" |
1346 show "?Q2 \<mapsto> ?P3" |
1351 apply(simp add: assert_imp_def) |
1347 apply(simp add: assert_imp_def) |
1352 done |
1348 done |
1353 next |
1349 next |
1382 apply(rule_tac x = na in exI) |
1378 apply(rule_tac x = na in exI) |
1383 apply(simp add: replicate_Suc tape_of_nl_abv) |
1379 apply(simp add: replicate_Suc tape_of_nl_abv) |
1384 done |
1380 done |
1385 qed |
1381 qed |
1386 next |
1382 next |
1387 show "{?P3} dither" |
1383 show "{?P3} dither \<up>" |
1388 using Hoare_unhalt_def |
1384 using Hoare_unhalt_def |
1389 proof(auto) |
1385 proof(auto) |
1390 fix nd n |
1386 fix nd n |
1391 assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" |
1387 assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" |
1392 thus "False" |
1388 thus "False" |