
diff -r cd4ef33c8fb1 -r 0838b0ac52ab thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sat Jan 19 14:44:07 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 19 15:27:21 2013 +0000
@@ -95,6 +95,65 @@
   shows "steps c p (m + n) = steps (steps c p m) p n"
 by (induct m arbitrary: c) (auto)
 
+lemma step_0 [simp]: 
+  shows "step (0, (l, r)) p = (0, (l, r))"
+by (case_tac p, simp)
+
+lemma steps_0 [simp]: 
+  shows "steps (0, (l, r)) p n = (0, (l, r))"
+by (induct n) (simp_all)
+
+
+
+fun
+  is_final :: "config \<Rightarrow> bool"
+where
+  "is_final (s, l, r) = (s = 0)"
+
+lemma is_final_eq: 
+  shows "is_final (s, tp) = (s = 0)"
+by (case_tac tp) (auto)
+
+lemma is_final_steps:
+  assumes "is_final (s, l, r)"
+  shows "is_final (steps (s, l, r) (p, off) n)"
+using assms 
+by (induct n) (auto)
+
+
+(* if the machine is in the halting state, there must have 
+   been a state just before the halting state *)
+lemma before_final: 
+  assumes "steps0 (1, tp) A n = (0, tp')"
+  shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+using assms
+proof(induct n arbitrary: tp')
+  case (0 tp')
+  have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
+  then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+    by simp
+next
+  case (Suc n tp')
+  have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
+    \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
+  have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
+  obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
+    by (auto intro: is_final.cases)
+  then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+  proof (cases "s = 0")
+    case True (* in halting state *)
+    then have "steps0 (1, tp) A n = (0, tp')"
+      using asm cases by (simp del: steps.simps)
+    then show ?thesis using ih by simp
+  next
+    case False (* not in halting state *)
+    then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
+      using asm cases by simp
+    then show ?thesis by auto
+  qed
+qed
+
+(* well-formedness of Turing machine programs *)
 fun 
   tm_wf :: "tprog \<Rightarrow> bool"
 where
@@ -135,117 +194,54 @@
   "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
 
 lemma length_shift [simp]: 
-  "length (shift p n) = length p"
+  shows "length (shift p n) = length p"
 by simp
 
-lemma length_adjust[simp]: 
+lemma length_adjust [simp]: 
   shows "length (adjust p) = length p"
 by (induct p) (auto)
 
+
+(* composition of two Turing machines *)
 fun
   tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
 where
   "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
 
-lemma step_0 [simp]: 
-  shows "step (0, (l, r)) p = (0, (l, r))"
-by (case_tac p, simp)
-
-lemma steps_0 [simp]: 
-  shows "steps (0, (l, r)) p n = (0, (l, r))"
-by (induct n) (simp_all)
-
-fun
-  is_final :: "config \<Rightarrow> bool"
-where
-  "is_final (s, l, r) = (s = 0)"
-
-lemma is_final_steps:
-  assumes "is_final (s, l, r)"
-  shows "is_final (steps (s, l, r) (p, off) n)"
-using assms by (induct n) (auto)
-
-
-
-(* if the machine is in the halting state, there must have 
-   been a state just before the halting state *)
-lemma before_final: 
-  assumes "steps0 (1, tp) A n = (0, tp')"
-  shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
-using assms
-proof(induct n arbitrary: tp')
-  case (0 tp')
-  have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
-  then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
-    by simp
-next
-  case (Suc n tp')
-  have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
-    \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
-  have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
-  obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
-    by (auto intro: is_final.cases)
-  then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
-  proof (cases "s = 0")
-    case True (* in halting state *)
-    then have "steps0 (1, tp) A n = (0, tp')"
-      using asm cases by (simp del: steps.simps)
-    then show ?thesis using ih by simp
-  next
-    case False (* not in halting state *)
-    then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
-      using asm cases by simp
-    then show ?thesis by auto
-  qed
-qed
-
-
-lemma length_comp:
+lemma tm_comp_length:
   shows "length (A |+| B) = length A + length B"
 by auto
 
-declare steps.simps[simp del]
-declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
-
-
-lemma tmcomp_fetch_in_first:
+lemma tm_comp_fetch_in_first:
   assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
   shows "fetch (A |+| B) a x = fetch A a x"
 using assms
-apply(case_tac a, case_tac [!] x, 
-auto simp: length_comp tm_comp.simps length_adjust nth_append)
-apply(simp_all add: adjust.simps)
-done
-
-
-lemma is_final_eq: "is_final (ba, tp) = (ba = 0)"
-apply(case_tac tp, simp add: is_final.simps)
+apply(case_tac a)
+apply(case_tac [!] x) 
+apply(auto simp: tm_comp_length nth_append)
 done
 
 lemma t_merge_pre_eq_step: 
-  assumes step: "step (a, b, c) (A, 0) = cf"
+  assumes step: "step0 (s, l, r) A = cf"
   and     tm_wf: "tm_wf (A, 0)" 
   and     unfinal: "\<not> is_final cf"
-  shows "step (a, b, c) (A |+| B, 0) = cf"
+  shows "step0 (s, l, r) (A |+| B) = cf"
 proof -
-  have "fetch (A |+| B) a (read c) = fetch A a (read c)"
-  proof(rule_tac tmcomp_fetch_in_first)
-    from step and unfinal show "case fetch A a (read c) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
-      apply(auto simp: is_final.simps)
-      apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq)
-      done
-  qed      
-  thus "?thesis"
-    using step
-    apply(auto simp: step.simps is_final.simps)
-    done
+  from step unfinal
+  have "\<not> is_final (step0 (s, l, r) A)" by simp
+  then  have "fetch (A |+| B) s (read r) = fetch A s (read r)"
+    by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq)
+  then show ?thesis
+    using step by auto
 qed
 
+declare steps.simps[simp del]
+declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
 declare tm_wf.simps[simp del] step.simps[simp del]
 
 lemma t_merge_pre_eq:  
-  "\<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>
-  \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf"
+  "\<lbrakk>steps0 (Suc 0, tp) A stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>
+  \<Longrightarrow> steps0 (Suc 0, tp) (A |+| B) stp = cf"
 proof(induct stp arbitrary: cf, simp add: steps.simps)
   fix stp cf
   assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk> 
@@ -280,7 +276,7 @@
   shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))"
 using assms
 apply(case_tac a, case_tac [!] x, 
-auto simp: length_comp tm_comp.simps length_adjust nth_append)
+auto simp: tm_comp_length tm_comp.simps length_adjust nth_append)
 apply(simp_all add: adjust.simps)
 done
 
@@ -376,7 +372,7 @@
      \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)"
 apply(case_tac x)
 apply(case_tac [!] sa',
-  auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps
+  auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
              tm_wf.simps shift.simps split: if_splits)
 done 
 
@@ -385,7 +381,7 @@
      \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
 apply(case_tac x)
 apply(case_tac [!] sa,
-  auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps
+  auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
              tm_wf.simps shift.simps split: if_splits)
 done 
 




