207 shows "steps (0, (l, r)) p n = (0, (l, r))" |
207 shows "steps (0, (l, r)) p n = (0, (l, r))" |
208 by (induct n) (simp_all) |
208 by (induct n) (simp_all) |
209 |
209 |
210 declare steps.simps[simp del] |
210 declare steps.simps[simp del] |
211 |
211 |
212 lemma before_final: |
212 lemma before_final_old: |
213 assumes "steps (1, tp) A n = (0, tp')" |
213 assumes "steps (1, tp) A n = (0, tp')" |
214 obtains n' where "\<not> is_final (steps (1, tp) A n')" |
214 obtains n' where "\<not> is_final (steps (1, tp) A n')" |
215 and "steps (1, tp) A (Suc n') = (0, tp')" |
215 and "steps (1, tp) A (Suc n') = (0, tp')" |
216 proof - |
216 proof - |
217 from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> |
217 from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> |
221 assume ind: |
221 assume ind: |
222 "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow> |
222 "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow> |
223 \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
223 \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
224 and h: " steps (1, tp) A (Suc n) = (0, tp')" |
224 and h: " steps (1, tp) A (Suc n) = (0, tp')" |
225 from h show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
225 from h show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
226 (* |
|
227 apply(simp add: step_red del: steps.simps) |
|
228 apply(case_tac "(steps (Suc 0, tp) A n)") |
|
229 apply(case_tac "a = 0") |
|
230 apply(simp) |
|
231 *) |
226 proof(simp add: step_red del: steps.simps, |
232 proof(simp add: step_red del: steps.simps, |
227 case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) |
233 case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) |
228 fix a b c |
234 fix a b c |
229 assume " steps (Suc 0, tp) A n = (0, tp')" |
235 assume " steps (Suc 0, tp) A n = (0, tp')" |
230 hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
236 hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
238 assume "steps (Suc 0, tp) A n = (a, b, c)" |
244 assume "steps (Suc 0, tp) A n = (a, b, c)" |
239 "step (steps (Suc 0, tp) A n) A = (0, tp')" |
245 "step (steps (Suc 0, tp) A n) A = (0, tp')" |
240 "a \<noteq> 0" |
246 "a \<noteq> 0" |
241 thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> |
247 thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> |
242 step (steps (Suc 0, tp) A n') A = (0, tp')" |
248 step (steps (Suc 0, tp) A n') A = (0, tp')" |
243 apply(rule_tac x = n in exI, simp) |
249 apply(rule_tac x = n in exI) |
|
250 apply(simp) |
244 done |
251 done |
245 qed |
252 qed |
246 qed |
253 qed |
247 thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n'); |
254 thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n'); |
248 steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
255 steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
249 by auto |
256 by auto |
|
257 qed |
|
258 |
|
259 lemma before_final: |
|
260 assumes "steps (1, tp) A n = (0, tp')" |
|
261 shows "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
262 using assms |
|
263 proof(induct n arbitrary: tp') |
|
264 case (0 tp') |
|
265 have asm: "steps (1, tp) A 0 = (0, tp')" by fact |
|
266 then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
267 by (simp add: steps.simps) |
|
268 next |
|
269 case (Suc n tp') |
|
270 have ih: "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow> |
|
271 \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" by fact |
|
272 have asm: "steps (1, tp) A (Suc n) = (0, tp')" by fact |
|
273 obtain s l r where cases: "steps (1, tp) A n = (s, l, r)" |
|
274 by (auto intro: is_final.cases) |
|
275 then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
|
276 proof (cases "s = 0") |
|
277 case True (* in halting state *) |
|
278 then have "steps (1, tp) A n = (0, tp')" |
|
279 using asm cases by simp |
|
280 then show ?thesis using ih by simp |
|
281 next |
|
282 case False (* not in halting state *) |
|
283 then have "\<not> is_final (steps (1, tp) A n) \<and> steps (1, tp) A (Suc n) = (0, tp')" |
|
284 using asm cases by simp |
|
285 then show ?thesis by auto |
|
286 qed |
250 qed |
287 qed |
251 |
288 |
252 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
289 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
253 |
290 |
254 lemma length_comp: |
291 lemma length_comp: |