--- a/Paper/Paper.thy	Wed Jan 30 23:00:09 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 23:57:33 2013 +0000
@@ -891,7 +891,7 @@
   "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
   @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to 
   each state of @{term tcopy_begin}, we define the
-  following invariant for the whole program:
+  following invariant for the whole @{term tcopy_begin} program:
 
   \begin{figure}
   \begin{center}

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Wed Jan 30 23:00:09 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 23:57:33 2013 +0000
@@ -104,8 +104,23 @@
 apply(simp_all add: assms)
 done
 
+(*
 lemma begin_partial_correctness:
-  assumes "\<exists>stp. steps0 cf tcopy_begin stp = (0, l, r)"
+  assumes "\<exists>stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
+  shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
+using assms 
+apply(auto simp add: Hoare_halt_def)
+apply(rule_tac x="stp" in exI)
+apply(simp)
+apply(case_tac "steps0 (Suc 0, [], Oc \<up> n) tcopy_begin stp")
+apply(simp)
+apply(case_tac n)
+apply(simp)
+apply(simp)
+apply(case_tac nat)
+apply(simp)
+apply(simp)
+*)
 
 fun measure_begin_state :: "config \<Rightarrow> nat"
   where