--- a/thys/uncomputable.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -63,14 +63,16 @@
 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))"
 
+
+
 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
-  "inv_begin n (s, l, r) = 
-        (if s = 0 then inv_begin0 n (l, r) else
-         if s = 1 then inv_begin1 n (l, r) else
-         if s = 2 then inv_begin2 n (l, r) else
-         if s = 3 then inv_begin3 n (l, r) else
-         if s = 4 then inv_begin4 n (l, r) 
+  "inv_begin n (s, tp) = 
+        (if s = 0 then inv_begin0 n tp else
+         if s = 1 then inv_begin1 n tp else
+         if s = 2 then inv_begin2 n tp else
+         if s = 3 then inv_begin3 n tp else
+         if s = 4 then inv_begin4 n tp 
          else False)"
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
@@ -120,8 +122,13 @@
 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
 by (case_tac r, auto, case_tac a, auto)
 
+
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
 lemma begin_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)"
+  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
 proof(rule_tac LE = begin_LE in halt_lemma) 
   show "wf begin_LE" unfolding begin_LE_def by (auto) 
 next
@@ -155,22 +162,22 @@
 qed
     
 lemma begin_correct: 
-  "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
+  "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
 proof(rule_tac Hoare_haltI)
   fix l r
-  assume h: "0 < x" "inv_begin1 x (l, r)"
-  hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
+  assume h: "0 < n" "inv_begin1 n (l, r)"
+  then have "\<exists> stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
     by (rule_tac begin_halt)    
-  then obtain stp where "is_final (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
-  moreover have "inv_begin x (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+  then obtain stp where "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" ..
+  moreover have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
     apply(rule_tac inv_begin_steps)
     using h by(simp_all add: inv_begin.simps)
   ultimately show
-    "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> 
-    inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n"
+    "\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and> 
+    inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
     using h
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
+    apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
     done
 qed
 
@@ -893,8 +900,11 @@
     by (metis assms loop_correct) 
   moreover
   have "inv_begin0 x \<mapsto> inv_loop1 x"
-    by (auto simp: inv_begin0.simps inv_loop1.simps assert_imp_def)
-       (rule_tac x = "Suc 0" in exI, auto)
+    unfolding assert_imp_def
+    unfolding inv_begin0.simps inv_loop1.simps
+    unfolding inv_loop1_loop.simps inv_loop1_exit.simps
+    apply(auto simp add: numeral Cons_eq_append_conv)
+    by (rule_tac x = "Suc 0" in exI, auto)
   ultimately 
   have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
     by (rule_tac Hoare_plus_halt) (auto)
@@ -922,10 +932,10 @@
     by (rule tcopy_correct1) (simp)
   moreover
   have "pre_tcopy n = inv_begin1 (Suc n)" 
-    by (auto simp add: tape_of_nl_abv)
+    by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
   moreover
   have "inv_end0 (Suc n) = post_tcopy n" 
-    by (auto simp add: inv_end0.simps tape_of_nl_abv)
+    by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nl_abv)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
     by simp