# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358953055 -3600
# Node ID 01e00065f6a26ad96c7168859d4d767ed5d6e206
# Parent  140489a4020e6423b72c412b7adb2c83b3482f5c
tuned

diff -r 140489a4020e -r 01e00065f6a2 thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 23 15:42:47 2013 +0100
+++ b/thys/uncomputable.thy	Wed Jan 23 15:57:35 2013 +0100
@@ -31,26 +31,49 @@
   The {\em Copying} TM, which duplicates its input. 
 *}
 
-definition tcopy_init :: "instr list"
+definition 
+  tcopy_init :: "instr list"
+where
+  "tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
+                 (W1, 3), (L, 4), (L, 4), (L, 0)]"
+
+definition 
+  tcopy_loop :: "instr list"
 where
-"tcopy_init \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
-               (W1, 3), (L, 4), (L, 4), (L, 0)]"
+  "tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),
+                 (R, 3), (R, 4), (W1, 5), (R, 4),
+                 (L, 6), (L, 5), (L, 6), (L, 1)]"
+
+definition 
+  tcopy_end :: "instr list"
+where
+  "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),
+                (R, 2), (R, 2), (L, 5), (W0, 4),
+                (R, 0), (L, 5)]"
+
+definition 
+  tcopy :: "instr list"
+where
+  "tcopy \<equiv> (tcopy_init |+| tcopy_loop) |+| tcopy_end"
+
+
+(* tcopy_init *)
 
 fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
-   "inv_init1 x (l, r) = (l = [] \<and> r = Oc\<up>x )"
+   "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)"
+  "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 = [])"
+  "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])))"
+  "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
@@ -182,11 +205,8 @@
     done
 qed
 
-definition tcopy_loop :: "instr list"
-where
-"tcopy_loop \<equiv> [(R, 0), (R, 2),  (R, 3), (W0, 2),
-                (R, 3), (R, 4), (W1, 5), (R, 4),
-                 (L, 6), (L, 5), (L, 6), (L, 1)]"
+
+(* tcopy_loop *)
 
 fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
@@ -692,13 +712,10 @@
       simp add: inv_init.simps inv_loop.simps)
     done
 qed
+
+
+(* tcopy_end *)
   
-definition tcopy_end :: "instr list"
-  where
-  "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),
-                (R, 2), (R, 2), (L, 5), (W0, 4),
-                (R, 0), (L, 5)]"
-
 fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
   where
   "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
@@ -979,9 +996,7 @@
     done
 qed
 
-definition tcopy :: "instr list"
-  where
-  "tcopy = ((tcopy_init |+| tcopy_loop) |+| tcopy_end)"
+(* tcopy *)
 
 lemma [intro]: "tm_wf (tcopy_init, 0)"
 by(auto simp: tm_wf.simps tcopy_init_def)
@@ -1160,16 +1175,13 @@
     done
 qed
 
-lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys"
-by auto
-
 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"
-apply(auto simp: tinres_def replicate_add[THEN sym])
-apply(case_tac "nb \<ge> n")
-apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
-apply arith
-apply(drule_tac length_eq, simp)
-done
+  apply(auto simp: tinres_def replicate_add[THEN sym])
+  apply(case_tac "nb \<ge> n")
+  apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)
+  apply arith
+  apply(drule_tac length_eq, simp)
+  done
 
 
 text {*
@@ -1290,14 +1302,14 @@
   ----------------------------
      {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
   ------------------------------------------------
-           {P1} tcontra {P3}
+                 {P1} tcontra {P3}
   *)
 
   have H_wf: "tm_wf0 (tcopy |+| H)" by auto
 
   (* {P1} (tcopy |+| H) {P3} *)
   have first: "{P1} (tcopy |+| H) {P3}" 
-  proof (induct rule: Hoare_plus_halt_simple)
+  proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
       by (rule tcopy_correct1) (simp)
@@ -1360,14 +1372,14 @@
   ----------------------------
      {P1} (tcopy |+| H) {P3}     {P3} dither loops
   ------------------------------------------------
-           {P1} tcontra loops
+               {P1} tcontra loops
   *)
 
   have H_wf: "tm_wf0 (tcopy |+| H)" by auto
 
   (* {P1} (tcopy |+| H) {P3} *)
   have first: "{P1} (tcopy |+| H) {P3}" 
-  proof (induct rule: Hoare_plus_halt_simple)
+  proof (cases rule: Hoare_plus_halt_simple)
     case A_halt (* of tcopy *)
     have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
       by (rule tcopy_correct1) (simp)