112 |
112 |
113 lemma is_final_eq: |
113 lemma is_final_eq: |
114 shows "is_final (s, tp) = (s = 0)" |
114 shows "is_final (s, tp) = (s = 0)" |
115 by (case_tac tp) (auto) |
115 by (case_tac tp) (auto) |
116 |
116 |
117 lemma is_final_steps: |
117 lemma after_is_final: |
118 assumes "is_final (s, l, r)" |
118 assumes "is_final c" |
119 shows "is_final (steps (s, l, r) (p, off) n)" |
119 shows "is_final (steps c p n)" |
120 using assms |
120 using assms |
121 by (induct n) (auto) |
121 apply(induct n) |
122 |
122 apply(case_tac [!] c) |
|
123 apply(auto) |
|
124 done |
|
125 |
|
126 lemma not_is_final: |
|
127 assumes a: "\<not> is_final (steps c p n1)" |
|
128 and b: "n2 \<le> n1" |
|
129 shows "\<not> is_final (steps c p n2)" |
|
130 proof (rule notI) |
|
131 obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add) |
|
132 assume "is_final (steps c p n2)" |
|
133 then have "is_final (steps c p n1)" unfolding eq |
|
134 by (simp add: after_is_final) |
|
135 with a show "False" by simp |
|
136 qed |
123 |
137 |
124 (* if the machine is in the halting state, there must have |
138 (* if the machine is in the halting state, there must have |
125 been a state just before the halting state *) |
139 been a state just before the halting state *) |
126 lemma before_final: |
140 lemma before_final: |
127 assumes "steps0 (1, tp) A n = (0, tp')" |
141 assumes "steps0 (1, tp) A n = (0, tp')" |
210 |
224 |
211 lemma tm_comp_length: |
225 lemma tm_comp_length: |
212 shows "length (A |+| B) = length A + length B" |
226 shows "length (A |+| B) = length A + length B" |
213 by auto |
227 by auto |
214 |
228 |
215 lemma tm_comp_step_aux: |
229 lemma tm_comp_step: |
216 assumes unfinal: "\<not> is_final (step0 c A)" |
230 assumes unfinal: "\<not> is_final (step0 c A)" |
217 shows "step0 c (A |+| B) = step0 c A" |
231 shows "step0 c (A |+| B) = step0 c A" |
218 proof - |
232 proof - |
219 obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) |
233 obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) |
220 have "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp |
234 have "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp |
245 by (metis is_final_eq step_0 surj_pair) |
259 by (metis is_final_eq step_0 surj_pair) |
246 |
260 |
247 have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" |
261 have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" |
248 by (simp only: step_red) |
262 by (simp only: step_red) |
249 also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2]) |
263 also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2]) |
250 also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step_aux[OF fin1]) |
264 also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1]) |
251 finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)" |
265 finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)" |
252 by (simp only: step_red) |
266 by (simp only: step_red) |
253 qed |
267 qed |
254 |
268 |
255 lemma tm_comp_fetch_in_A: |
269 lemma tm_comp_fetch_in_A: |
317 proof - |
331 proof - |
318 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
332 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
319 obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')" |
333 obtain stp' where fin: "\<not> is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')" |
320 using before_final[OF a_ht] by blast |
334 using before_final[OF a_ht] by blast |
321 from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'" |
335 from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'" |
322 by (rule tm_comp_step) |
336 by (rule tm_comp_steps) |
323 from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')" |
337 from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')" |
324 by (simp only: step_red) |
338 by (simp only: step_red) |
325 |
339 |
326 have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" |
340 have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" |
327 by (simp only: step_red) |
341 by (simp only: step_red) |