equal
deleted
inserted
replaced
3750 \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0" |
3750 \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0" |
3751 apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto) |
3751 apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto) |
3752 done |
3752 done |
3753 |
3753 |
3754 lemma [simp]: "left (trpl l st r) = l" |
3754 lemma [simp]: "left (trpl l st r) = l" |
3755 apply(simp add: left.simps trpl.simps lo.simps |
3755 apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp) |
3756 loR.simps mod_dvd_simp, auto simp: conf_decode1) |
3756 apply(auto simp: conf_decode1) |
3757 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r", |
3757 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r") |
3758 auto) |
3758 apply(auto) |
3759 apply(erule_tac x = l in allE, auto) |
3759 apply(erule_tac x = l in allE, auto) |
3760 done |
3760 done |
3761 |
3761 |
3762 lemma [simp]: "stat (trpl l st r) = st" |
3762 lemma [simp]: "stat (trpl l st r) = st" |
3763 apply(simp add: stat.simps trpl.simps lo.simps |
3763 apply(simp add: stat.simps trpl.simps lo.simps |
4611 |
4611 |
4612 lemma F_correct: |
4612 lemma F_correct: |
4613 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4613 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4614 tm_wf (tp,0); 0<rs\<rbrakk> |
4614 tm_wf (tp,0); 0<rs\<rbrakk> |
4615 \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4615 \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
|
4616 thm halt_least_step nonstop_t_eq nonstop_lemma rec_t_eq_steps conf_lemma |
4616 apply(frule_tac halt_least_step, auto) |
4617 apply(frule_tac halt_least_step, auto) |
4617 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4618 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4618 using rec_t_eq_steps[of tp l lm stp] |
4619 using rec_t_eq_steps[of tp l lm stp] |
4619 apply(simp add: conf_lemma) |
4620 apply(simp add: conf_lemma) |
4620 proof - |
4621 proof - |