--- 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)