equal
deleted
inserted
replaced
166 then show ?thesis by auto |
166 then show ?thesis by auto |
167 qed |
167 qed |
168 qed |
168 qed |
169 |
169 |
170 (* well-formedness of Turing machine programs *) |
170 (* well-formedness of Turing machine programs *) |
|
171 abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0" |
|
172 |
171 fun |
173 fun |
172 tm_wf :: "tprog \<Rightarrow> bool" |
174 tm_wf :: "tprog \<Rightarrow> bool" |
173 where |
175 where |
174 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
176 "tm_wf (p, off) = (length p \<ge> 2 \<and> is_even (length p) \<and> |
175 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
177 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
176 |
178 |
177 abbreviation |
179 abbreviation |
178 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
180 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
179 |
|
180 |
181 |
181 lemma halt_lemma: |
182 lemma halt_lemma: |
182 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
183 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
183 by (metis wf_iff_no_infinite_down_chain) |
184 by (metis wf_iff_no_infinite_down_chain) |
184 |
185 |
347 also have "... = (Suc (length A div 2), tp')" |
348 also have "... = (Suc (length A div 2), tp')" |
348 by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]]) |
349 by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]]) |
349 finally show thesis using a by blast |
350 finally show thesis using a by blast |
350 qed |
351 qed |
351 |
352 |
352 |
|
353 |
|
354 lemma tm_comp_fetch_second_zero: |
353 lemma tm_comp_fetch_second_zero: |
355 assumes h1: "fetch B s x = (a, 0)" |
354 assumes h1: "fetch B s x = (a, 0)" |
356 and hs: "tm_wf (A, 0)" "s \<noteq> 0" |
355 and hs: "tm_wf (A, 0)" "s \<noteq> 0" |
357 shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)" |
356 shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)" |
358 using h1 hs |
357 using h1 hs |
370 apply(case_tac [!] sa) |
369 apply(case_tac [!] sa) |
371 apply(auto simp: tm_comp_length nth_append) |
370 apply(auto simp: tm_comp_length nth_append) |
372 done |
371 done |
373 |
372 |
374 |
373 |
375 lemma t_merge_second_same: |
374 lemma tm_comp_second_same: |
376 assumes a_wf: "tm_wf (A, 0)" |
375 assumes a_wf: "tm_wf (A, 0)" |
377 and steps: "steps0 (1, l, r) B stp = (s', l', r')" |
376 and steps: "steps0 (1, l, r) B stp = (s', l', r')" |
378 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp |
377 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp |
379 = (if s' = 0 then 0 else s' + length A div 2, l', r')" |
378 = (if s' = 0 then 0 else s' + length A div 2, l', r')" |
380 using steps |
379 using steps |
412 done |
411 done |
413 } |
412 } |
414 ultimately show ?case by blast |
413 ultimately show ?case by blast |
415 qed |
414 qed |
416 |
415 |
417 lemma t_merge_second_halt_same: |
416 lemma tm_comp_second_halt_same: |
418 assumes "tm_wf (A, 0)" |
417 assumes "tm_wf (A, 0)" |
419 and "steps0 (1, l, r) B stp = (0, l', r')" |
418 and "steps0 (1, l, r) B stp = (0, l', r')" |
420 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" |
419 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" |
421 using t_merge_second_same[OF assms] by (simp) |
420 using tm_comp_second_same[OF assms] by (simp) |
422 |
421 |
423 end |
422 end |
424 |
423 |