--- a/thys2/UF_Rec.thy	Sat May 25 01:32:35 2013 +0100
+++ b/thys2/UF_Rec.thy	Sat May 25 01:33:31 2013 +0100
@@ -699,47 +699,6 @@
 by (simp add: rec_uf_def)
 
 
-subsection {* Relating interperter functions to the execution of TMs *}
-
-lemma rec_step: 
-  assumes "(\<lambda> (s, l, r). s \<le> length tp div 2) c"
-  shows "Trpl_code (step0 c tp) = Newconf (Code tp) (Trpl_code c)"
-apply(cases c)
-apply(simp only: Trpl_code.simps)
-apply(simp only: Let_def step.simps)
-apply(case_tac "fetch tp (a - 0) (read ca)")
-apply(simp only: prod.cases)
-apply(case_tac "update aa (b, ca)")
-apply(simp only: prod.cases)
-apply(simp only: Trpl_code.simps)
-apply(simp only: Newconf.simps)
-apply(simp only: Left.simps)
-oops
-
-lemma rec_steps:
-  assumes "tm_wf0 tp"
-  shows "Trpl_code (steps0 (1, Bk \<up> l, <lm>) tp stp) = Conf stp (Code tp) (bl2wc (<lm>))"
-apply(induct stp)
-apply(simp)
-apply(simp)
-oops
-
-
-lemma F_correct: 
-  assumes tm: "steps0 (1, Bk \<up> l, <lm>) tp stp = (0, Bk \<up> m, Oc \<up> rs @ Bk \<up> n)"
-  and     wf:  "tm_wf0 tp" "0 < rs"
-  shows "rec_eval rec_uf [Code tp, bl2wc (<lm>)] = (rs - Suc 0)"
-proof -
-  from least_steps[OF tm] 
-  obtain stp_least where
-    before: "\<forall>stp' < stp_least. \<not> is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" and
-    after:  "\<forall>stp' \<ge> stp_least. is_final (steps0 (1, Bk \<up> l, <lm>) tp stp')" by blast
-  have "Halt (Code tp) (bl2wc (<lm>)) = stp_least" sorry
-  show ?thesis
-    apply(simp only: uf_lemma)
-    apply(simp only: UF.simps)
-    apply(simp only: Halt.simps)
-    oops
 
 
 end