diff -r dfe852aacae6 -r 06db15939b7c thys/abacus.thy
--- a/thys/abacus.thy	Wed Jan 30 03:46:22 2013 +0000
+++ b/thys/abacus.thy	Wed Jan 30 09:33:06 2013 +0000
@@ -1330,7 +1330,7 @@
 
 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)
                     else Oc\<up>(Suc m) @ Bk # <lm>)"
-apply(case_tac lm, simp_all add: tape_of_nl_abv  split: if_splits)
+apply(case_tac lm, simp_all add: tape_of_nl_abv  tape_of_nat_abv split: if_splits)
 done
 
 
@@ -1952,7 +1952,7 @@
 apply(auto simp: inv_on_left_moving_in_middle_B.simps 
                  inv_check_left_moving_on_leftmost.simps split: if_splits)
 apply(case_tac [!] "rev lm1", simp_all)
-apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
 done
 
 lemma [simp]:
@@ -2020,11 +2020,11 @@
 apply(erule_tac exE)+
 apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
       rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
-apply(case_tac [!] "rev lm1",simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps)
 apply(case_tac [!] a, simp_all)
-apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps, auto)
-apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps, auto)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_list.simps)
+apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps)
 done
 
 lemma [simp]: 
@@ -4295,8 +4295,8 @@
 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
 apply(subgoal_tac "length list = Suc q", auto)
 apply(subgoal_tac "drop q list = [list ! q]")
-apply(simp add: tape_of_nl_abv)
-by (metis append_Nil2 append_eq_conv_conj lessI nth_drop')
+apply(simp add: tape_of_nl_abv tape_of_nat_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI)
 
 lemma erase2jumpover2:
   "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>
@@ -4307,9 +4307,8 @@
 apply(erule_tac notE)
 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
 apply(subgoal_tac "length list = Suc q", auto)
-apply(erule_tac x = "n" in allE, simp)
-by (metis append_Nil2 append_eq_conv_conj lessI nth_drop'
-  replicate_Suc tape_of_nat_list.simps(2) tape_of_nl_abv) 
+apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons)
 
 lemma mopup_bef_erase_a_2_jump_over[simp]: 
  "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0;  s \<le> 2 * n;
@@ -4725,6 +4724,12 @@
 apply(rule mopup_a_nth, auto)
 done
 
+(* FIXME: is also in uncomputable *)
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
+
 lemma mopup_halt:
   assumes 
   less: "n < length lm"