diff -r e9ef4ada308b -r d8e6f0798e23 thys/UTM.thy
--- a/thys/UTM.thy	Thu Mar 14 20:43:43 2013 +0000
+++ b/thys/UTM.thy	Wed Mar 27 09:47:02 2013 +0000
@@ -1214,22 +1214,11 @@
 apply(simp add: t_twice_def mopup.simps t_twice_compile_def)
 done
 
-lemma [intro]: "rec_calc_rel (recf.id (Suc 0) 0) [rs] rs"
-  apply(rule_tac calc_id, simp_all)
-  done
-  
-lemma [intro]: "rec_calc_rel (constn 2) [rs] 2"
-using prime_rel_exec_eq[of "constn 2" "[rs]" 2]
-apply(subgoal_tac "primerec (constn 2) 1", auto)
-done
-
-lemma  [intro]: "rec_calc_rel rec_mult [rs, 2] (2 * rs)"
-using prime_rel_exec_eq[of "rec_mult" "[rs, 2]"  "2*rs"]
-apply(subgoal_tac "primerec rec_mult (Suc (Suc 0))", auto)
-done
-
 declare start_of.simps[simp del]
 
+lemma twice_lemma: "rec_exec rec_twice [rs] = 2*rs"
+by(auto simp: rec_twice_def rec_exec.simps)
+
 lemma t_twice_correct: 
   "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) 
   (tm_of abc_twice @ shift (mopup (Suc 0)) ((length (tm_of abc_twice) div 2))) stp =
@@ -1237,28 +1226,23 @@
 proof(case_tac "rec_ci rec_twice")
   fix a b c
   assume h: "rec_ci rec_twice = (a, b, c)"
-  have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup 1) 
-    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (2*rs)) @ Bk\<up>(l))"
-  proof(rule_tac recursive_compile_to_tm_correct)
+  have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_twice @ shift (mopup (length [rs])) 
+    (length (tm_of abc_twice) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_twice [rs])) @ Bk\<up>(l))"
+    thm  recursive_compile_to_tm_correct1
+  proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_twice = (a, b, c)" by (simp add: h)
   next
-    show "rec_calc_rel rec_twice [rs] (2 * rs)"
-      apply(simp add: rec_twice_def)
-      apply(rule_tac rs =  "[rs, 2]" in calc_cn, simp_all)
-      apply(rule_tac allI, case_tac k, auto)
-      done
+    show "terminate rec_twice [rs]"
+      apply(rule_tac primerec_terminate, auto)
+      apply(simp add: rec_twice_def, auto simp: constn.simps numeral_2_eq_2)
+      by(auto)
   next
-    show "length [rs] = 1" by simp
-  next	
-    show "layout_of (a [+] dummy_abc 1) = layout_of (a [+] dummy_abc 1)" by simp
-  next
-    show "tm_of abc_twice = tm_of (a [+] dummy_abc 1)"
+    show "tm_of abc_twice = tm_of (a [+] dummy_abc (length [rs]))"
       using h
-      apply(simp add: abc_twice_def)
-      done
+      by(simp add: abc_twice_def)
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv rec_exec.simps twice_lemma)
     done
 qed
 
@@ -1386,8 +1370,7 @@
 
 lemma [simp]: " tm_wf (t_twice_compile, 0)"
 apply(simp only: t_twice_compile_def)
-apply(rule_tac t_compiled_correct)
-apply(simp_all add: abc_twice_def)
+apply(rule_tac wf_tm_from_abacus, simp)
 done
 
 lemma t_twice_change_term_state:
@@ -1503,7 +1486,7 @@
     apply(rule_tac x = stp in exI, rule_tac x = "ln + lna" in exI, 
           rule_tac x = rn in exI)
     apply(simp add: t_wcode_main_def)
-    apply(simp add: replicate_Suc[THEN sym] exp_add[THEN sym] del: replicate_Suc)
+    apply(simp add: replicate_Suc[THEN sym] replicate_add [THEN sym] del: replicate_Suc)
     done
   from this obtain stpb lnb rnb where stp2: 
     "steps0 (13, Bk # Bk # Bk\<up>(lna) @ Oc # ires, Oc\<up>(Suc (Suc rs)) @ Bk\<up>(rna)) t_wcode_main stpb =
@@ -2018,15 +2001,13 @@
 apply(simp add: t_fourtimes_len_def t_fourtimes_def mopup.simps t_fourtimes_compile_def)
 done
 
-lemma [intro]: "rec_calc_rel (constn 4) [rs] 4"
-using prime_rel_exec_eq[of "constn 4" "[rs]" 4]
-apply(subgoal_tac "primerec (constn 4) 1", auto)
-done
-
-lemma [intro]: "rec_calc_rel rec_mult [rs, 4] (4 * rs)"
-using prime_rel_exec_eq[of "rec_mult" "[rs, 4]"  "4*rs"]
-apply(subgoal_tac "primerec rec_mult 2", auto simp: numeral_2_eq_2)
-done
+lemma [intro]: "primerec rec_fourtimes (Suc 0)"
+apply(auto simp: rec_fourtimes_def numeral_4_eq_4 constn.simps)
+by auto
+
+lemma fourtimes_lemma: "rec_exec rec_fourtimes [rs] = 4 * rs"
+by(simp add: rec_exec.simps rec_fourtimes_def)
+
 
 lemma t_fourtimes_correct: 
   "\<exists>stp ln rn. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) 
@@ -2035,35 +2016,28 @@
 proof(case_tac "rec_ci rec_fourtimes")
   fix a b c
   assume h: "rec_ci rec_fourtimes = (a, b, c)"
-  have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup 1) 
-    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (4*rs)) @ Bk\<up>(l))"
-  proof(rule_tac recursive_compile_to_tm_correct)
+  have "\<exists>stp m l. steps0 (Suc 0, Bk # Bk # ires, <[rs]> @ Bk\<up>(n)) (tm_of abc_fourtimes @ shift (mopup (length [rs])) 
+    (length (tm_of abc_fourtimes) div 2)) stp = (0, Bk\<up>(m) @ Bk # Bk # ires, Oc\<up>(Suc (rec_exec rec_fourtimes [rs])) @ Bk\<up>(l))"
+    thm recursive_compile_to_tm_correct1
+  proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_fourtimes = (a, b, c)" by (simp add: h)
   next
-    show "rec_calc_rel rec_fourtimes [rs] (4 * rs)"
-      apply(simp add: rec_fourtimes_def)
-      apply(rule_tac rs =  "[rs, 4]" in calc_cn, simp_all)
-      apply(rule_tac allI, case_tac k, auto simp: mult_lemma)
-      done
+    show "terminate rec_fourtimes [rs]"
+      apply(rule_tac primerec_terminate)
+      by auto
   next
-    show "length [rs] = 1" by simp
-  next	
-    show "layout_of (a [+] dummy_abc 1) = layout_of (a [+] dummy_abc 1)" by simp
-  next
-    show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc 1)"
+    show "tm_of abc_fourtimes = tm_of (a [+] dummy_abc (length [rs]))"
       using h
-      apply(simp add: abc_fourtimes_def)
-      done
+      by(simp add: abc_fourtimes_def)
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv fourtimes_lemma)
     done
 qed
 
 lemma wf_fourtimes[intro]: "tm_wf (t_fourtimes_compile, 0)"
 apply(simp only: t_fourtimes_compile_def)
-apply(rule_tac t_compiled_correct)
-apply(simp_all add: abc_twice_def)
+apply(rule_tac wf_tm_from_abacus, simp)
 done
 
 lemma t_fourtimes_change_term_state:
@@ -2175,7 +2149,7 @@
              = (L, Suc 0)" 
 apply(subgoal_tac "14 = Suc 13")
 apply(simp only: fetch.simps add_Suc nth_of.simps t_wcode_main_def)
-apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def)
+apply(simp add:length_append length_shift Parity.two_times_even_div_two even_twice_len t_fourtimes_len_def nth_append)
 by arith
 
 lemma [simp]: "fetch t_wcode_main (14 + length t_twice div 2 + t_fourtimes_len) Bk
@@ -2228,7 +2202,7 @@
     apply(rule_tac x = stp in exI, 
           rule_tac x = "ln + lna" in exI,
           rule_tac x = rn in exI, simp)
-    apply(simp add: replicate_Suc[THEN sym] exp_add[THEN sym] del: replicate_Suc)
+    apply(simp add: replicate_Suc[THEN sym] replicate_add[THEN sym] del: replicate_Suc)
     done
   from this obtain stpb lnb rnb where stp2:
     "steps0 (t_twice_len + 14, Bk # Bk # Bk\<up>(lna) @ Oc # ires, Oc\<up>(Suc (rs + 1)) @ Bk\<up>(rna))
@@ -2254,8 +2228,6 @@
     done
 qed
 
-(**********************************************************)
-
 fun wcode_on_left_moving_3_B :: "bin_inv_t"
   where
   "wcode_on_left_moving_3_B ires rs (l, r) = 
@@ -4742,7 +4714,7 @@
 apply(rule_tac x = "Suc m" in exI, simp only: exp_ind)
 apply(simp only: exp_ind, simp)
 apply(subgoal_tac "m = length la + nata")
-apply(rule_tac x = "m - nata" in exI, simp add: exp_add)
+apply(rule_tac x = "m - nata" in exI, simp add: replicate_add)
 apply(drule_tac length_equal, simp)
 apply(simp only: exp_ind[THEN sym] replicate_Suc[THEN sym] replicate_add[THEN sym])
 apply(rule_tac x = "m + Suc (Suc n)" in exI, simp)
@@ -4757,40 +4729,36 @@
 proof -
   obtain ap arity fp where a: "rec_ci rec_F = (ap, arity, fp)"
     by (metis prod_cases3) 
-  moreover have b: "rec_calc_rel  rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+  moreover have b: "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
     using assms
     apply(rule_tac F_correct, simp_all)
     done 
   have "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
-    (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)"  
-  proof(rule_tac recursive_compile_to_tm_correct)
+    (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)"  
+  proof(rule_tac recursive_compile_to_tm_correct1)
     show "rec_ci rec_F = (ap, arity, fp)" using a by simp
   next
-    show "rec_calc_rel rec_F [code tp, bl2wc (<lm>)] (rs - 1)"
-      using b by simp
-  next
-    show "length [code tp, bl2wc (<lm>)] = 2" by simp
+    show "terminate rec_F [code tp, bl2wc (<lm>)]"
+      using assms
+      by(rule_tac terminate_F, simp_all)
   next
-    show "layout_of (ap [+] dummy_abc 2) = layout_of (ap [+] dummy_abc 2)"
-      by simp
-  next
-    show "F_tprog = tm_of (ap [+] dummy_abc 2)"
+    show "F_tprog = tm_of (ap [+] dummy_abc (length [code tp, bl2wc (<lm>)]))"
       using a
       apply(simp add: F_tprog_def F_aprog_def numeral_2_eq_2)
       done
   qed
   then obtain stp m l where 
     "steps0 (Suc 0, Bk # Bk # [], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
-    (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
-    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rs - 1) @ Bk\<up>l)" by blast
+    (F_tprog @ shift (mopup (length [code tp, (bl2wc (<lm>))])) (length F_tprog div 2)) stp
+    = (0, Bk\<up>m @ Bk # Bk # [], Oc\<up>Suc (rec_exec rec_F [code tp, (bl2wc (<lm>))]) @ Bk\<up>l)" by blast
   hence "\<exists> m. steps0 (Suc 0, [Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>i)
     (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp
     = (0, Bk\<up>m, Oc\<up>Suc (rs - 1) @ Bk\<up>l)"
   proof -
     assume g: "steps0 (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk \<up> i)
-      (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp =
-      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc (rs - 1) @ Bk \<up> l)"
+      (F_tprog @ shift (mopup (length [code tp, bl2wc (<lm>)])) (length F_tprog div 2)) stp =
+      (0, Bk \<up> m @ [Bk, Bk], Oc \<up> Suc ((rec_exec rec_F [code tp, bl2wc (<lm>)])) @ Bk \<up> l)"
    moreover have "tinres [Bk, Bk] [Bk]"
      apply(auto simp: tinres_def)
      done
@@ -4800,7 +4768,8 @@
     (F_tprog @ shift (mopup 2) (length F_tprog div 2)) stp", auto)
       done
     ultimately show "?thesis"
-      apply(drule_tac tinres_steps1, auto)
+      using b
+      apply(drule_tac la = "Bk\<up>m @ [Bk, Bk]" in tinres_steps1, auto simp: numeral_2_eq_2)
       done
   qed
   thus "?thesis"
@@ -4819,7 +4788,7 @@
       
 lemma [intro]: "tm_wf (t_utm, 0)"
 apply(simp only: t_utm_def F_tprog_def)
-apply(rule_tac t_compiled_correct, auto)
+apply(rule_tac wf_tm_from_abacus, auto)
 done 
 
 lemma UTM_halt_lemma_pre: 
@@ -4993,141 +4962,162 @@
 lemma nonstop_true:
   "\<lbrakk>tm_wf (tp, 0);
   \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-  \<Longrightarrow> \<forall>y. rec_calc_rel rec_nonstop 
-  ([code tp, bl2wc (<lm>), y]) (Suc 0)"
+  \<Longrightarrow> \<forall>y. rec_exec rec_nonstop ([code tp, bl2wc (<lm>), y]) =  (Suc 0)"
 apply(rule_tac allI, erule_tac x = y in allE)
 apply(case_tac "steps0 (Suc 0, Bk\<up>(l), <lm>) tp y", simp)
 apply(rule_tac nonstop_t_uhalt_eq, simp_all)
 done
 
-declare ci_cn_para_eq[simp]
+lemma cn_arity:  "rec_ci (Cn n f gs) = (a, b, c) \<Longrightarrow> b = n"
+by(case_tac "rec_ci f", simp add: rec_ci.simps)
+
+lemma mn_arity: "rec_ci (Mn n f) = (a, b, c) \<Longrightarrow> b = n"
+by(case_tac "rec_ci f", simp add: rec_ci.simps)
 
 lemma F_aprog_uhalt: 
-  "\<lbrakk>tm_wf (tp,0); 
-    \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp)); 
-    rec_ci rec_F = (F_ap, rs_pos, a_md)\<rbrakk>
-  \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos )
-               @ suflm) (F_ap) stp of (ss, e) \<Rightarrow> ss < length (F_ap)"
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf 
-               ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])")
-apply(simp only: rec_F_def, rule_tac i = 0  and ga = a and gb = b and 
-  gc = c in cn_gi_uhalt, simp, simp, simp, simp, simp, simp, simp)
-apply(simp add: ci_cn_para_eq)
-apply(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf 
-  ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))")
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) rec_conf
-              ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])])" 
-           and n = "Suc (Suc 0)" and f = rec_right and 
-          gs = "[Cn (Suc (Suc 0)) rec_conf 
-           ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]"
-           and i = 0 and ga = aa and gb = ba and gc = ca in 
-          cn_gi_uhalt)
-apply(simp, simp, simp, simp, simp, simp, simp, 
-     simp add: ci_cn_para_eq)
-apply(case_tac "rec_ci rec_halt")
-apply(rule_tac rf = "(Cn (Suc (Suc 0)) rec_conf 
-  ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt]))" 
-  and n = "Suc (Suc 0)" and f = "rec_conf" and 
-  gs = "([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])"  and 
-  i = "Suc (Suc 0)" and gi = "rec_halt" and ga = ab and gb = bb and
-  gc = cb in cn_gi_uhalt)
-apply(simp, simp, simp, simp, simp add: nth_append, simp, 
-  simp add: nth_append, simp add: rec_halt_def)
-apply(simp only: rec_halt_def)
-apply(case_tac [!] "rec_ci ((rec_nonstop))")
-apply(rule_tac allI, rule_tac impI, simp)
-apply(case_tac j, simp)
-apply(rule_tac x = "code tp" in exI, rule_tac calc_id, simp, simp, simp, simp)
-apply(rule_tac x = "bl2wc (<lm>)" in exI, rule_tac calc_id, simp, simp, simp)
-apply(rule_tac rf = "Mn (Suc (Suc 0)) (rec_nonstop)"
-  and f = "(rec_nonstop)" and n = "Suc (Suc 0)"
-  and  aprog' = ac and rs_pos' =  bc and a_md' = cc in Mn_unhalt)
-apply(simp, simp add: rec_halt_def , simp, simp)
-apply(drule_tac  nonstop_true, simp_all)
-apply(rule_tac allI)
-apply(erule_tac x = y in allE)+
-apply(simp)
-done
+  assumes wf_tm: "tm_wf (tp,0)"
+   and unhalt:  "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))"
+   and compile: "rec_ci rec_F = (F_ap, rs_pos, a_md)"
+ shows "{\<lambda> nl. nl = [code tp, bl2wc (<lm>)] @ 0\<up>(a_md - rs_pos ) @ suflm} (F_ap) \<up>"
+  using compile
+proof(simp only: rec_F_def)
+  assume h: "rec_ci (Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) 
+    rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]]) =
+    (F_ap, rs_pos, a_md)"
+  moreover hence "rs_pos = Suc (Suc 0)"
+    using cn_arity 
+    by simp
+  moreover obtain ap1 ar1 ft1 where a: "rec_ci 
+    (Cn (Suc (Suc 0)) rec_right 
+    [Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]]) = (ap1, ar1, ft1)"
+    by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0)) 
+      rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt]])", auto)
+  moreover hence b: "ar1 = Suc (Suc 0)"
+    using cn_arity by simp
+  ultimately show "?thesis"
+  proof(rule_tac i = 0 in cn_unhalt_case, auto)
+    fix anything
+    obtain ap2 ar2 ft2 where c: 
+      "rec_ci (Cn (Suc (Suc 0)) rec_conf [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])
+      = (ap2, ar2, ft2)" 
+      by(case_tac "rec_ci (Cn (Suc (Suc 0)) rec_conf
+        [recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), rec_halt])", auto)
+    moreover hence d:"ar2 = Suc (Suc 0)"
+      using cn_arity by simp
+    ultimately have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>"
+      using a b c d
+    proof(rule_tac i = 0 in cn_unhalt_case, auto)
+      fix anything
+      obtain ap3 ar3 ft3 where e: "rec_ci rec_halt = (ap3, ar3, ft3)"
+        by(case_tac "rec_ci rec_halt", auto)
+      hence f: "ar3 = Suc (Suc 0)"
+        using mn_arity
+        by(simp add: rec_halt_def)
+      have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
+        using c d e f
+      proof(rule_tac i = 2 in cn_unhalt_case, auto simp: rec_halt_def)
+        fix anything
+        have "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>"
+          using e f
+        proof(rule_tac mn_unhalt_case, auto simp: rec_halt_def)
+          fix i
+          show "terminate rec_nonstop [code tp, bl2wc (<lm>), i]"
+            by(rule_tac primerec_terminate, auto)
+        next
+          fix i
+          show "0 < rec_exec rec_nonstop [code tp, bl2wc (<lm>), i]"
+            using assms
+            by(drule_tac nonstop_true, auto)
+        qed
+        thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft3 - Suc (Suc 0)) @ anything} ap3 \<up>" by simp
+      next
+        fix apj arj ftj j  anything
+        assume "j<2" "rec_ci ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) = (apj, arj, ftj)"
+        hence "{\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @ 0 \<up> (ftj - arj) @ anything} apj
+          {\<lambda>nl. nl = [code tp, bl2wc (<lm>)] @
+            rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 
+               0 \<up> (ftj - Suc arj) @ anything}"
+          apply(rule_tac recursive_compile_correct)
+          apply(case_tac j, auto)
+          apply(rule_tac [!] primerec_terminate)
+          by(auto)
+        thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ftj - arj) @ anything} apj
+          {\<lambda>nl. nl = code tp # bl2wc (<lm>) # rec_exec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0))
+          (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j) [code tp, bl2wc (<lm>)] # 0 \<up> (ftj - Suc arj) @ anything}"
+          by simp
+      next
+        fix j
+        assume "(j::nat) < 2"
+        thus "terminate ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0), Mn (Suc (Suc 0)) rec_nonstop] ! j)
+          [code tp, bl2wc (<lm>)]"
+          by(case_tac j, auto intro!: primerec_terminate)
+      qed
+      thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft2 - Suc (Suc 0)) @ anything} ap2 \<up>"
+        by simp
+    qed
+    thus "{\<lambda>nl. nl = code tp # bl2wc (<lm>) # 0 \<up> (ft1 - Suc (Suc 0)) @ anything} ap1 \<up>" by simp
+  qed
+qed
 
 lemma uabc_uhalt': 
   "\<lbrakk>tm_wf (tp, 0);
   \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp));
   rec_ci rec_F = (ap, pos, md)\<rbrakk>
-  \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap stp of (ss, e)
-           \<Rightarrow>  ss < length ap"
+  \<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} ap \<up>"
 proof(frule_tac F_ap = ap and rs_pos = pos and a_md = md
-    and suflm = "[]" in F_aprog_uhalt, auto)
-  fix stp a b
+    and suflm = "[]" in F_aprog_uhalt, auto simp: abc_Hoare_unhalt_def, 
+     case_tac "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap n", simp)
+  fix n a b
   assume h: 
-    "\<forall>stp. case abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp of 
-    (ss, e) \<Rightarrow> ss < length ap"
-    "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap stp = (a, b)" 
+    "\<forall>n. abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
+    "abc_steps_l (0, [code tp, bl2wc (<lm>)]) ap n = (a, b)" 
     "tm_wf (tp, 0)" 
     "rec_ci rec_F = (ap, pos, md)"
-  moreover have "ap \<noteq> []"
-    using h apply(rule_tac rec_ci_not_null, simp)
-    done
+  moreover have a: "ap \<noteq> []"
+    using h rec_ci_not_null[of "rec_F" pos md] by auto
   ultimately show "a < length ap"
-  proof(erule_tac x = stp in allE,
-  case_tac "abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp", simp)
-    fix aa ba
-    assume g: "aa < length ap" 
-      "abc_steps_l (0, code tp # bl2wc (<lm>) # 0\<up>(md - pos)) ap stp = (aa, ba)" 
-      "ap \<noteq> []"
+  proof(erule_tac x = n in allE)
+    assume g: "abc_notfinal (abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n) ap"
+    obtain ss nl where b : "abc_steps_l (0, code tp # bl2wc (<lm>) # 0 \<up> (md - pos)) ap n = (ss, nl)"
+      by (metis prod.exhaust)
+    then have c: "ss < length ap"
+      using g by simp
     thus "?thesis"
+      using a b c
       using abc_list_crsp_steps[of "[code tp, bl2wc (<lm>)]"
-                                   "md - pos" ap stp aa ba] h
-      apply(simp)
-      done
+                                   "md - pos" ap n ss nl] h
+      by(simp)
   qed
 qed
 
 lemma uabc_uhalt: 
   "\<lbrakk>tm_wf (tp, 0); 
   \<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <lm>) tp stp))\<rbrakk>
-  \<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog 
-       stp of (ss, e) \<Rightarrow> ss < length F_aprog"
+  \<Longrightarrow> {\<lambda> nl. nl = [code tp, bl2wc (<lm>)]} F_aprog \<up> "
 apply(case_tac "rec_ci rec_F", simp add: F_aprog_def)
 apply(drule_tac ap = a and pos = b and md = c in uabc_uhalt', simp_all)
-proof -
-  fix a b c
-  assume 
-    "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) a stp of (ss, e) 
-                                                   \<Rightarrow> ss < length a"
-    "rec_ci rec_F = (a, b, c)"
-  thus 
-    "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) 
-    (a [+] dummy_abc (Suc (Suc 0))) stp of (ss, e) \<Rightarrow> 
-           ss < Suc (Suc (Suc (length a)))"
-    using abc_append_uhalt1[of a "[code tp, bl2wc (<lm>)]" 
-      "a [+] dummy_abc (Suc (Suc 0))" "[]" "dummy_abc (Suc (Suc 0))"]  
-    apply(simp)
-    done
-qed
+apply(rule_tac abc_Hoare_plus_unhalt1, simp)
+done
 
 lemma tutm_uhalt': 
 assumes tm_wf:  "tm_wf (tp,0)"
   and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (1, Bk\<up>(l), <lm>) tp stp))"
   shows "\<forall> stp. \<not> is_final (steps0 (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp)"
 unfolding t_utm_def
-proof(rule_tac compile_correct_unhalt)
-  show "layout_of F_aprog = layout_of F_aprog" by simp
-next
+proof(rule_tac compile_correct_unhalt, auto)
   show "F_tprog = tm_of F_aprog"
     by(simp add:  F_tprog_def)
 next
-  show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (1, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
+  show "crsp (layout_of F_aprog) (0, [code tp, bl2wc (<lm>)]) (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>)  []"
     by(auto simp: crsp.simps start_of.simps)
 next
-  show "length F_tprog div 2 = length F_tprog div 2" by simp
-next
-  show "\<forall>stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp of (as, am) \<Rightarrow> as < length F_aprog"
+  fix stp a b
+  show "abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp = (a, b) \<Longrightarrow> a < length F_aprog"
     using assms
-    apply(erule_tac uabc_uhalt, simp)
-    done
+    apply(drule_tac uabc_uhalt, auto simp: abc_Hoare_unhalt_def)
+    by(erule_tac x = stp in allE, erule_tac x = stp in allE, simp) 
 qed
 
- 
 lemma tinres_commute: "tinres r r' \<Longrightarrow> tinres r' r"
 apply(auto simp: tinres_def)
 done
@@ -5166,7 +5156,7 @@
 apply(case_tac "m > Suc (Suc 0)")
 apply(rule_tac x = "m - Suc (Suc 0)" in exI) 
 apply(case_tac m, simp_all add: , case_tac nat, simp_all add: replicate_Suc)
-apply(rule_tac x = "2 - m" in exI, simp add: exp_add[THEN sym])
+apply(rule_tac x = "2 - m" in exI, simp add: replicate_add[THEN sym])
 apply(simp only: numeral_2_eq_2, simp add: replicate_Suc)
 done
 
@@ -5330,4 +5320,5 @@
 using assms(2-3)
 apply(simp add: tape_of_nat_abv)
 done
+
 end                               
\ No newline at end of file