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