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 *) |
|
232 proof(simp add: step_red del: steps.simps, |
226 proof(simp add: step_red del: steps.simps, |
233 case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) |
227 case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp) |
234 fix a b c |
228 fix a b c |
235 assume " steps (Suc 0, tp) A n = (0, tp')" |
229 assume " steps (Suc 0, tp) A n = (0, tp')" |
236 hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |
230 hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" |