equal
deleted
inserted
replaced
994 and the final configuration is standard. |
994 and the final configuration is standard. |
995 *} |
995 *} |
996 |
996 |
997 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
997 definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool" |
998 where |
998 where |
999 "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n. tp = (Bk \<up> k, <n::nat>)))}" |
999 "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}" |
1000 |
1000 |
1001 lemma [intro, simp]: "tm_wf0 tcopy" |
1001 lemma [intro, simp]: "tm_wf0 tcopy" |
1002 by (auto simp: tcopy_def) |
1002 by (auto simp: tcopy_def) |
1003 |
1003 |
1004 lemma [intro, simp]: "tm_wf0 dither" |
1004 lemma [intro, simp]: "tm_wf0 dither" |
1106 unfolding Hoare_halt_def |
1106 unfolding Hoare_halt_def |
1107 apply(auto) |
1107 apply(auto) |
1108 apply(drule_tac x = n in spec) |
1108 apply(drule_tac x = n in spec) |
1109 apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n") |
1109 apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n") |
1110 apply(auto simp add: tape_of_nl_abv) |
1110 apply(auto simp add: tape_of_nl_abv) |
1111 done |
1111 by (metis append_Nil2 replicate_0) |
1112 qed |
1112 qed |
1113 |
1113 |
1114 (* asumme tcontra halts on its code *) |
1114 (* asumme tcontra halts on its code *) |
1115 lemma tcontra_halt: |
1115 lemma tcontra_halt: |
1116 assumes "haltP tcontra [code tcontra]" |
1116 assumes "haltP tcontra [code tcontra]" |