diff -r aeaf1374dc67 -r 5317c92ff2a7 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Tue Jan 29 12:37:06 2013 +0000
+++ b/thys/uncomputable.thy	Tue Jan 29 13:00:51 2013 +0000
@@ -65,11 +65,11 @@
   inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
   "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>   
-                         (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
+                          (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
 | "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])))"
+| "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
@@ -83,11 +83,13 @@
 
 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> 
   \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
-apply(rule_tac x = "Suc i" in exI, simp)
-done
+by (rule_tac x = "Suc i" in exI, simp)
 
 lemma inv_begin_step: 
-  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
+  assumes "inv_begin x cf"
+  and "x > 0"
+  shows "inv_begin x (step0 cf tcopy_begin)"
+using assms
 unfolding tcopy_begin_def
 apply(case_tac cf)
 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
@@ -96,11 +98,14 @@
 done
 
 lemma inv_begin_steps: 
-  "\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk>
- \<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)"
-apply(induct stp, simp add: steps.simps)
+  assumes "inv_begin x cf"
+  and "x > 0"
+  shows "inv_begin x (steps0 cf tcopy_begin stp)"
+apply(induct stp)
+apply(simp add: steps.simps assms)
 apply(auto simp: step_red)
-apply(rule_tac inv_begin_step, simp_all)
+apply(rule_tac inv_begin_step)
+apply(simp_all add: assms)
 done
 
 fun begin_state :: "config \<Rightarrow> nat"
@@ -136,28 +141,28 @@
 by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
 
 lemma begin_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], 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" by(simp add: wf_begin_le)
 next
   assume h: "0 < x"
-  show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
-        (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-            steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
+  show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
+        (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
+            steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
   proof(rule_tac allI, rule_tac impI)
     fix n
-    assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
-    have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
+    assume a: "\<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
+    have b: "inv_begin x (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
       apply(rule_tac inv_begin_steps)
       apply(simp_all add: inv_begin.simps h)
       done 
-    obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
-      apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
+    obtain s l r where c: "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
+      apply(case_tac "steps (1, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
       done
     moreover hence "inv_begin x (s, l, r)" 
       using c b by simp
-    ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
-      steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
+    ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), 
+      steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
       using a 
     proof(simp del: inv_begin.simps)
       assume "inv_begin x (s, l, r)" "0 < s"
@@ -174,10 +179,10 @@
 proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x" "inv_begin1 x (l, r)"
-  hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
+  hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
     by (rule_tac begin_halt)    
-  then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
-  moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+  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)"
     apply(rule_tac inv_begin_steps)
     using h by(simp_all add: inv_begin.simps)
   ultimately show
@@ -185,7 +190,7 @@
     inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n"
     using h
     apply(rule_tac x = stp in exI)
-    apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
+    apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
     done
 qed