702 subsection {* Relating interperter functions to the execution of TMs *}

   703 

   704 lemma rec_step: 

   705   assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c"

   706   shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"

   707 apply(cases c)

   708 apply(simp only: Trpl_code.simps)

   709 apply(simp only: Let_def step.simps)

   710 apply(case_tac "fetch tp (a - 0) (read ca)")

   711 apply(simp only: prod.cases)

   712 apply(case_tac "update aa (b, ca)")

   713 apply(simp only: prod.cases)

   714 apply(simp only: Trpl_code.simps)

   715 apply(simp only: Newconf.simps)

   716 apply(simp only: Left.simps)

   717 oops

   718 

   719 lemma rec_steps:

   720   assumes "tm_wf0 tp"

   721   shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"

   722 apply(induct stp)

   723 apply(simp)

   724 apply(simp)

   725 oops

   726 

   727 

   728 lemma F_correct: 

   729   assumes tm: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"

   730   and     wf:  "tm_wf0 tp" "0 < rs"

   731   shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"

   732 proof -

   733   from least_steps[OF tm] 

   734   obtain stp_least where

   735     before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and

   736     after:  "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast

   737   have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry

   738   show ?thesis

   739     apply(simp only: uf_lemma)

   740     apply(simp only: UF.simps)

   741     apply(simp only: Halt.simps)

   742     oops