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