# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358623422 0
# Node ID be5187b73ab9366aeaea538c6f84f720c9fbdc29
# Parent  0838b0ac52ab88f3141b78fdd2d5a817da67bf83
more proofs polished

diff -r 0838b0ac52ab -r be5187b73ab9 paper.pdf
Binary file paper.pdf has changed
diff -r 0838b0ac52ab -r be5187b73ab9 thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sat Jan 19 15:27:21 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 19 19:23:42 2013 +0000
@@ -240,35 +240,35 @@
 declare tm_wf.simps[simp del] step.simps[simp del]
 
 lemma t_merge_pre_eq:  
-  "\<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> 
-    \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf"
-  and h: "steps (Suc 0, tp) (A, 0) (Suc stp) = cf"
-      "\<not> is_final cf" "tm_wf (A, 0)"
-  from h show "steps (Suc 0, tp) (A |+| B, 0) (Suc stp) = cf"
-  proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp)
-    fix a b c
-    assume g: "steps (Suc 0, tp) (A, 0) stp = (a, b, c)"
-      "step (a, b, c) (A, 0) = cf"
-    have "(steps (Suc 0, tp) (A |+| B, 0) stp) = (a, b, c)"
-    proof(rule ind, simp_all add: h g)
-      show "0 < a"
-        using g h
-        apply(simp add: step_red)
-        apply(case_tac a, auto simp: step_0)
-        apply(case_tac "steps (Suc 0, tp) (A, 0) stp", simp)
-        done
-    qed
-    thus "step (steps (Suc 0, tp) (A |+| B, 0) stp) (A |+| B, 0) = cf"
-      apply(simp)
-      apply(rule_tac t_merge_pre_eq_step, simp_all add: g h)
-      done
-  qed
+  assumes "steps0 (1, tp) A stp = cf" 
+  and "\<not> is_final cf" 
+  and wf_A: "tm_wf (A, 0)"
+  shows "steps0 (1, tp) (A |+| B) stp = cf"
+using assms(1) assms(2)
+proof(induct stp arbitrary: cf)
+  case (0 cf)
+  then show "steps0 (1, tp) (A |+| B) 0 = cf"
+    by (auto simp: steps.simps)
+next 
+  case (Suc stp cf)
+  have ih: "\<And>cf. \<lbrakk>steps0 (1, tp) A stp = cf; \<not> is_final cf\<rbrakk> \<Longrightarrow> steps0 (1, tp) (A |+| B) stp = cf" by fact
+  then obtain s l r where eq: "steps0 (1, tp) A stp = (s, l, r)"
+    by (metis is_final.cases)
+  have fin: "\<not> is_final cf" by fact
+
+  have "steps0 (1, tp) A (Suc stp) = cf" by fact
+  then have "step0 (steps0 (1, tp) A stp) A = cf" by simp 
+  then have h: "step0 (s, l, r) A = cf" using eq by simp
+  then have "\<not> is_final (s, l, r)" using fin by (cases s) (auto)
+  then have eq2: "steps0 (1, tp) (A |+| B) stp = (s, l, r)" by (rule ih[OF eq])
+  
+  have "steps0 (1, tp) (A |+| B) (Suc stp) = step0 (steps0 (Suc 0, tp) (A |+| B) stp) (A |+| B)" by simp
+  also have "... = step0 (s, l, r) (A |+| B)" using eq2 by simp
+  also have "... = cf" by (rule t_merge_pre_eq_step[OF h wf_A fin])
+  finally show "steps0 (1, tp) (A |+| B) (Suc stp) = cf" .
 qed
 
+
 lemma tmcomp_fetch_in_first2:
   assumes "fetch A a x = (ac, 0)"
           "tm_wf (A, 0)"
@@ -354,7 +354,7 @@
   proof(simp add: step_red)
     assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')"
            " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')"
-    moreover hence "(steps (Suc 0, tp) (A |+| B, 0) stp') = (steps (Suc 0, tp) (A, 0) stp')"
+    moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')"
       apply(rule_tac t_merge_pre_eq)
       apply(simp_all add: a_wf a_ht)
       done