--- 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