diff -r fbd346f5af86 -r 30950dadd09f thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sat Jan 19 21:03:55 2013 +0000
+++ b/thys/turing_basic.thy	Sun Jan 20 05:04:19 2013 +0000
@@ -212,7 +212,7 @@
   shows "length (A |+| B) = length A + length B"
 by auto
 
-lemma tm_comp_pre_eq_step: 
+lemma tm_comp_step_aux: 
   assumes unfinal: "\<not> is_final (step0 c A)"
   shows "step0 c (A |+| B) = step0 c A"
 proof -
@@ -228,202 +228,179 @@
   then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) 
 qed
 
-lemma tm_comp_pre_eq:  
-  assumes "\<not> is_final (steps0 (1, tp) A n)" 
-  shows "steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n"
+lemma tm_comp_step:  
+  assumes "\<not> is_final (steps0 c A n)" 
+  shows "steps0 c (A |+| B) n = steps0 c A n"
 using assms
 proof(induct n)
   case 0
-  then show "steps0 (1, tp) (A |+| B) 0 = steps0 (1, tp) A 0" by auto
+  then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto
 next 
   case (Suc n)
-  have ih: "\<not> is_final (steps0 (1, tp) A n) \<Longrightarrow> steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" by fact
-  have fin: "\<not> is_final (steps0 (1, tp) A (Suc n))" by fact
-  then have fin1: "\<not> is_final (step0 (steps0 (1, tp) A n) A)" 
+  have ih: "\<not> is_final (steps0 c A n) \<Longrightarrow> steps0 c (A |+| B) n = steps0 c A n" by fact
+  have fin: "\<not> is_final (steps0 c A (Suc n))" by fact
+  then have fin1: "\<not> is_final (step0 (steps0 c A n) A)" 
     by (auto simp only: step_red)
-  then have fin2: "\<not> is_final (steps0 (1, tp) A n)"
+  then have fin2: "\<not> is_final (steps0 c A n)"
     by (metis is_final_eq step_0 surj_pair) 
  
-  have "steps0 (1, tp) (A |+| B) (Suc n) = step0 (steps0 (1, tp) (A |+| B) n) (A |+| B)" 
+  have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" 
     by (simp only: step_red)
-  also have "... = step0 (steps0 (1, tp) A n) (A |+| B)" by (simp only: ih[OF fin2])
-  also have "... = step0 (steps0 (1, tp) A n) A" by (simp only: tm_comp_pre_eq_step[OF fin1])
-  finally show "steps0 (1, tp) (A |+| B) (Suc n) = steps0 (1, tp) A (Suc n)"
+  also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2])
+  also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step_aux[OF fin1])
+  finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)"
     by (simp only: step_red)
 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 tmcomp_fetch_in_first2:
-  assumes "fetch A a x = (ac, 0)"
-          "tm_wf (A, 0)"
-          "a \<le> length A div 2" "a > 0"
-  shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))"
-using assms
-apply(case_tac a, case_tac [!] x, 
-auto simp: tm_comp_length tm_comp.simps length_adjust nth_append)
-apply(simp_all add: adjust.simps)
+lemma tm_comp_fetch_in_A:
+  assumes h1: "fetch A s x = (a, 0)"
+  and h2: "s \<le> length A div 2" 
+  and h3: "s \<noteq> 0"
+  shows "fetch (A |+| B) s x = (a, Suc (length A div 2))"
+using h1 h2 h3
+apply(case_tac s)
+apply(case_tac [!] x)
+apply(auto simp: tm_comp_length nth_append)
 done
 
-lemma tmcomp_exec_after_first:
-  "\<lbrakk>0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); 
-       a \<le> length A div 2\<rbrakk>
-       \<Longrightarrow> step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')"
-apply(simp add: step.simps, auto)
-apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2)
-apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2)
-done
-
-lemma step_nothalt_pre: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c);  0 < a\<rbrakk> \<Longrightarrow> 0 < aa"
-apply(case_tac "aa = 0", simp add: step_0, simp)
+lemma tm_comp_exec_after_first:
+  assumes h1: "\<not> is_final c" 
+  and h2: "step0 c A = (0, tp)"
+  and h3: "fst c \<le> length A div 2"
+  shows "step0 c (A |+| B) = (Suc (length A div 2), tp)"
+using h1 h2 h3
+apply(case_tac c)
+apply(auto simp del: tm_comp.simps)
+apply(case_tac "fetch A a Bk")
+apply(simp del: tm_comp.simps)
+apply(subst tm_comp_fetch_in_A)
+apply(auto)[4]
+apply(case_tac "fetch A a (hd c)")
+apply(simp del: tm_comp.simps)
+apply(subst tm_comp_fetch_in_A)
+apply(auto)[4]
 done
 
-lemma nth_in_set: 
-  "\<lbrakk> A ! i = x; i <  length A\<rbrakk> \<Longrightarrow> x \<in> set A"
-by auto
-
-lemma step_nothalt: 
-  "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\<rbrakk> \<Longrightarrow> 
-  a \<le> length A div 2"
-apply(simp add: step.simps)
-apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps)
-apply(case_tac "A ! (2 * nat)", simp)
-apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)
-apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps)
-apply(case_tac "A ! (2 * nat)", simp)
-apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)
-apply(case_tac "A ! (Suc (2 * nat))")
-apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set)
+lemma step_in_range: 
+  assumes h1: "\<not> is_final (step0 c A)"
+  and h2: "tm_wf (A, 0)"
+  shows "fst (step0 c A) \<le> length A div 2"
+using h1 h2
+apply(case_tac c)
+apply(case_tac a)
+apply(auto simp add: prod_case_unfold Let_def)
+apply(case_tac "hd c")
+apply(auto simp add: prod_case_unfold)
 done
 
 lemma steps_in_range: 
-  " \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk>
-  \<Longrightarrow> a \<le> length A div 2"
-proof(induct stp arbitrary: a b c)
-  fix a b c
-  assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" 
-            "tm_wf (A, 0)"
-  thus "a \<le> length A div 2"
-    apply(simp add: steps.simps tm_wf.simps, auto)
-    done
+  assumes h1: "\<not> is_final (steps0 (1, tp) A stp)"
+  and h2: "tm_wf (A, 0)"
+  shows "fst (steps0 (1, tp) A stp) \<le> length A div 2"
+using h1
+proof(induct stp)
+  case 0
+  then show "fst (steps0 (1, tp) A 0) \<le> length A div 2" using h2
+    by (auto simp add: steps.simps tm_wf.simps)
 next
-  fix stp a b c
-  assume ind: "\<And>a b c. \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); 
-    tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2"
-  and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)"
-  from h show "a \<le> length A div 2"
-  proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp)
-    fix aa ba ca
-    assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" 
-           "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)"
-    hence "aa \<le> length A div 2"
-      apply(rule_tac ind, auto simp: h step_nothalt_pre)
-      done
-    thus "?thesis"
-      using g h
-      apply(rule_tac step_nothalt, auto)
-      done
-  qed
+  case (Suc stp)
+  have ih: "\<not> is_final (steps0 (1, tp) A stp) \<Longrightarrow> fst (steps0 (1, tp) A stp) \<le> length A div 2" by fact
+  have h: "\<not> is_final (steps0 (1, tp) A (Suc stp))" by fact
+  from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \<le> length A div 2"
+    by (metis step_in_range step_red)
 qed
 
-lemma t_merge_pre_halt_same: 
-  assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')"
+lemma tm_comp_pre_halt_same: 
+  assumes a_ht: "steps0 (1, tp) A n = (0, tp')"
   and a_wf: "tm_wf (A, 0)"
-  obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')"
+  obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')"
 proof -
   assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis"
-  obtain stp' where "\<not> is_final (steps (1, tp) (A, 0) stp')" and 
-                          "steps (1, tp) (A, 0) (Suc stp') = (0, tp')"
-  using a_ht before_final by blast
-  then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')"
-  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 "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')"
-      apply(rule_tac tm_comp_pre_eq)
-      apply(simp_all add: a_ht)
-      done
-    ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')"
-      apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp)
-      apply(rule tmcomp_exec_after_first, simp_all add: a_wf)
-      apply(erule_tac steps_in_range, auto simp: a_wf)
-      done
-  qed
-  with a show thesis by blast
+  obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')"
+  using before_final[OF a_ht] by blast
+  from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'"
+    by (rule tm_comp_step)
+  from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')"
+    by (simp only: step_red)
+
+  have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" 
+    by (simp only: step_red)
+  also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp
+  also have "... = (Suc (length A div 2), tp')" 
+    by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]])
+  finally show thesis using a by blast
 qed
 
+
+
 lemma tm_comp_fetch_second_zero:
-  "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk>
-     \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)"
+  assumes h1: "fetch B s x = (a, 0)"
+  and hs: "tm_wf (A, 0)" "s \<noteq> 0"
+  shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)"
+using h1 hs
 apply(case_tac x)
-apply(case_tac [!] sa',
-  auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
-             tm_wf.simps shift.simps split: if_splits)
+apply(case_tac [!] s)
+apply(auto simp: tm_comp_length nth_append)
 done 
 
 lemma tm_comp_fetch_second_inst:
-  "\<lbrakk>sa > 0; s > 0;  tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk>
-     \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
+  assumes h1: "fetch B sa x = (a, s)"
+  and hs: "tm_wf (A, 0)" "sa \<noteq> 0" "s \<noteq> 0"
+  shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
+using h1 hs
 apply(case_tac x)
-apply(case_tac [!] sa,
-  auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
-             tm_wf.simps shift.simps split: if_splits)
+apply(case_tac [!] sa)
+apply(auto simp: tm_comp_length nth_append)
 done 
 
+
 lemma t_merge_second_same:
   assumes a_wf: "tm_wf (A, 0)"
-  and b_wf: "tm_wf (B, 0)"
-  and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')"
-  shows "steps (Suc (length A div 2), l, r)  (A |+| B, 0) stp
-       = (if s = 0 then 0
-          else s + length A div 2, l', r')"
-using a_wf b_wf steps
-proof(induct stp arbitrary: s l' r', simp add: steps.simps, simp)
-  fix stpa sa l'a r'a
-  assume ind: "\<And>s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \<Longrightarrow>
-    steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = 
-                (if s = 0 then 0 else s + length A div 2, l', r')"
-  and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)"
-  obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')"
-    apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto)
-    done
-  from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = 
-                (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')"
-    apply(erule_tac ind)
+  and steps: "steps0 (1, l, r) B stp = (s', l', r')"
+  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp 
+    = (if s' = 0 then 0 else s' + length A div 2, l', r')"
+using steps
+proof(induct stp arbitrary: s' l' r')
+  case 0
+  then show ?case by (simp add: steps.simps)
+next
+  case (Suc stp s' l' r')
+  obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')"
+    by (metis is_final.cases)
+  then have ih1: "s'' = 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')"
+  and ih2: "s'' \<noteq> 0 \<Longrightarrow> steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')"
+    using Suc by (auto)
+  have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact
+
+  { assume "s'' = 0"
+    then have ?case using a h ih1 by (simp del: steps.simps) 
+  } moreover
+  { assume as: "s'' \<noteq> 0" "s' = 0"
+    from as a h 
+    have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps)
+    with as have ?case
+    apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps)
+    apply(case_tac "fetch B s'' (read r'')")
+    apply(auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] simp del: tm_comp.simps)
     done
-  from a b h show 
-    "(sa = 0 \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \<and>
-    (0 < sa \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))"
-  proof(case_tac "sa' = 0", auto)
-    assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'"
-    thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)"
-      using a_wf b_wf
-      apply(simp add:  step.simps)
-      apply(case_tac "fetch B sa' (read r'')", auto)
-      apply(simp_all add: step.simps tm_comp_fetch_second_zero)
-      done
-  next
-    assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa"
-    thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)"
-      using a_wf b_wf
-      apply(simp add: step.simps)
-      apply(case_tac "fetch B sa' (read r'')", auto)
-      apply(simp_all add: step.simps tm_comp_fetch_second_inst)
-      done
-  qed
+  } moreover
+  { assume as: "s'' \<noteq> 0" "s' \<noteq> 0"
+    from as a h
+    have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps)
+    with as have ?case
+    apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps)
+    apply(case_tac "fetch B s'' (read r'')")
+    apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps)
+    done
+  }
+  ultimately show ?case by blast
 qed
 
 lemma t_merge_second_halt_same:
-  "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0); 
-   steps (1, l, r) (B, 0) stp = (0, l', r')\<rbrakk>
-     \<Longrightarrow> steps (Suc (length A div 2), l, r)  (A |+| B, 0) stp
-       = (0, l', r')"
-using t_merge_second_same[where s = "0"]
-apply(auto)
-done
+  assumes "tm_wf (A, 0)"  
+  and "steps0 (1, l, r) B stp = (0, l', r')"
+  shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp = (0, l', r')"
+using t_merge_second_same[OF assms] by (simp)
 
-        
 end