--- a/thys/uncomputable.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/uncomputable.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -57,26 +57,19 @@
 
 (* tcopy_init *)
 
-fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-   "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-
-fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where 
-  "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-
-fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-
-fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
-
-fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
+fun 
+  inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
   "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
                          (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
+| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
+| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
+| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
+| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
 
 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
@@ -184,7 +177,7 @@
     
 lemma init_correct: 
   "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_init1 x (l, r)"
@@ -690,7 +683,7 @@
 
 lemma loop_correct:
   "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_loop1 x (l, r)"
@@ -973,7 +966,7 @@
 
 lemma end_correct:
   "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_end1 x (l, r)"
@@ -1060,7 +1053,7 @@
     by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
-    by (rule Hoare_weak)
+    by (rule Hoare_weaken)
 qed
 
 
@@ -1113,7 +1106,7 @@
 
 lemma dither_halts:
   shows "{dither_halt_inv} dither {dither_halt_inv}" 
-apply(rule HoareI)
+apply(rule Hoare_haltI)
 using dither_halt_rs
 apply(auto)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
@@ -1314,7 +1307,7 @@
     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
     using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
   then show "{pre_H_inv M n} H {post_H_halt_inv}"
-    unfolding Hoare_def
+    unfolding Hoare_halt_def
     apply(auto)
     apply(rule_tac x = stp in exI)
     apply(auto)
@@ -1329,7 +1322,7 @@
     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
     using h_newcase[of "M" "[n]" "1", OF assms] by auto 
   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
-    unfolding Hoare_def
+    unfolding Hoare_halt_def
     apply(auto)
     apply(rule_tac x = stp in exI)
     apply(auto)
@@ -1387,7 +1380,7 @@
   with assms show "False"
     unfolding P1_def P3_def
     unfolding haltP_def
-    unfolding Hoare_def 
+    unfolding Hoare_halt_def 
     apply(auto)
     apply(erule_tac x = n in allE)
     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")