--- a/thys/uncomputable.thy	Sun Jan 27 15:46:32 2013 +0000
+++ b/thys/uncomputable.thy	Sun Jan 27 17:15:38 2013 +0000
@@ -49,7 +49,7 @@
                 (R, 2), (R, 2), (L, 5), (W0, 4),
                 (R, 0), (L, 5)]"
 
-definition 
+idefinition 
   tcopy :: "instr list"
 where
   "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
@@ -81,16 +81,13 @@
          if s = 4 then inv_begin4 n (l, r) 
          else False)"
 
-
-
 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
 
 lemma inv_begin_step: 
-  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk>
- \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
+  "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
 unfolding tcopy_begin_def
 apply(case_tac cf)
 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
@@ -139,7 +136,7 @@
 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
 
 lemma init_halt: 
-  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+  "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
 proof(rule_tac LE = init_LE in halt_lemma)
   show "wf init_LE" by(simp add: wf_begin_le)
 next
@@ -173,13 +170,12 @@
 qed
     
 lemma init_correct: 
-  "x > 0 \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
+  "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
 proof(rule_tac Hoare_haltI)
   fix l r
-  assume h: "0 < x"
-    "inv_begin1 x (l, r)"
-  hence "\<exists> stp. is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
-    by(erule_tac init_halt)    
+  assume h: "0 < x" "inv_begin1 x (l, r)"
+  hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
+    by (rule_tac init_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)"
     apply(rule_tac inv_begin_steps)
@@ -1004,7 +1000,7 @@
 
 
 lemma dither_halts_aux: 
-  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 3 = (0, Bk \<up> m, [Oc, Oc])"
+  shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
 unfolding dither_def
 by (simp add: steps.simps step.simps numeral)