diff -r d5a0e25c4742 -r a9003e6d0463 thys/UF.thy
--- a/thys/UF.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/UF.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -2,10 +2,10 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Construction of a Universal Function *}
+chapter {* Construction of a Universal Function *}
 
 theory UF
-imports Rec_Def GCD Abacus
+imports Rec_Def HOL.GCD Abacus
 begin
 
 text {*
@@ -289,9 +289,6 @@
         arity.simps[simp del] Sigma.simps[simp del]
         rec_sigma.simps[simp del]
 
-lemma [simp]: "arity z = 1"
- by(simp add: arity.simps)
-
 lemma rec_pr_0_simp_rewrite: "
   rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
 by(simp add: rec_exec.simps)
@@ -341,7 +338,7 @@
              take_Suc_conv_app_nth)
 qed
     
-lemma [simp]: "primerec f n \<Longrightarrow> arity f = n"
+lemma arity_primerec[simp]: "primerec f n \<Longrightarrow> arity f = n"
   apply(case_tac f)
   apply(auto simp: arity.simps )
   apply(erule_tac prime_mn_reverse)
@@ -527,30 +524,28 @@
 apply(rule_tac Min_le, auto)
 done
 
-lemma [simp]: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}
+lemma expand_conj_in_set: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}
     = (if Rr (xs @ [Suc w]) then insert (Suc w) 
                               {x. x \<le> w \<and> Rr (xs @ [x])}
       else {x. x \<le> w \<and> Rr (xs @ [x])})"
 by(auto, case_tac "x = Suc w", auto)
 
-lemma [simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
-apply(simp add: Minr.simps, auto)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-done
-
-lemma [simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>  
+lemma Minr_strip_Suc[simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
+by(cases "\<forall>x\<le>w. \<not> Rr (xs @ [x])",auto simp add: Minr.simps expand_conj_in_set)
+
+lemma x_empty_set[simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>  
                            {x. x \<le> w \<and> Rr (xs @ [x])} = {} "
 by auto
 
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
+lemma Minr_is_Suc[simp]: "\<lbrakk>Minr Rr xs w = Suc w; Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
                                        Minr Rr xs (Suc w) = Suc w"
-apply(simp add: Minr.simps)
+apply(simp add: Minr.simps expand_conj_in_set)
 apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
 done
  
-lemma [simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
+lemma Minr_is_Suc_Suc[simp]: "\<lbrakk>Minr Rr xs w = Suc w; \<not> Rr (xs @ [Suc w])\<rbrakk> \<Longrightarrow> 
                                    Minr Rr xs (Suc w) = Suc (Suc w)"
-apply(simp add: Minr.simps)
+apply(simp add: Minr.simps expand_conj_in_set)
 apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
 apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<in> 
                                 {x. x \<le> w \<and> Rr (xs @ [x])}", simp)
@@ -612,50 +607,45 @@
 
 declare numeral_3_eq_3[simp]
 
-lemma [intro]: "primerec rec_pred (Suc 0)"
+lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)"
 apply(simp add: rec_pred_def)
 apply(rule_tac prime_cn, auto)
 apply(case_tac i, auto intro: prime_id)
 done
 
-lemma [intro]: "primerec rec_minus (Suc (Suc 0))"
+lemma primerec_rec_minus_2[intro]: "primerec rec_minus (Suc (Suc 0))"
   apply(auto simp: rec_minus_def)
   done
 
-lemma [intro]: "primerec (constn n) (Suc 0)"
+lemma primerec_constn_1[intro]: "primerec (constn n) (Suc 0)"
   apply(induct n)
   apply(auto simp: constn.simps intro: prime_z prime_cn prime_s)
   done
 
-lemma [intro]: "primerec rec_sg (Suc 0)" 
+lemma primerec_rec_sg_1[intro]: "primerec rec_sg (Suc 0)" 
   apply(simp add: rec_sg_def)
   apply(rule_tac k = "Suc (Suc 0)" in prime_cn, auto)
   apply(case_tac i, auto)
   apply(case_tac ia, auto intro: prime_id)
   done
 
-lemma [simp]: "length (get_fstn_args m n) = n"
-  apply(induct n)
-  apply(auto simp: get_fstn_args.simps)
-  done
-
-lemma  primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
+lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
 apply(induct n, auto simp: get_fstn_args.simps)
 apply(case_tac "i = n", auto simp: nth_append intro: prime_id)
 done
 
-lemma [intro]: "primerec rec_add (Suc (Suc 0))"
+lemma primerec_rec_add_2[intro]: "primerec rec_add (Suc (Suc 0))"
 apply(simp add: rec_add_def)
 apply(rule_tac prime_pr, auto)
 done
 
-lemma [intro]:"primerec rec_mult (Suc (Suc 0))"
+lemma primerec_rec_mult_2[intro]:"primerec rec_mult (Suc (Suc 0))"
 apply(simp add: rec_mult_def )
 apply(rule_tac prime_pr, auto intro: prime_z)
 apply(case_tac i, auto intro: prime_id)
 done  
 
-lemma [elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk>   \<Longrightarrow> 
+lemma primerec_ge_2_elim[elim]: "\<lbrakk>primerec rf n; n \<ge> Suc (Suc 0)\<rbrakk>   \<Longrightarrow> 
                         primerec (rec_accum rf) n"
 apply(auto simp: rec_accum.simps)
 apply(simp add: nth_append, auto)
@@ -670,11 +660,11 @@
   apply(auto, simp add: nth_append, auto)
   done
 
-lemma [simp]: "Rr (xs @ [0]) \<Longrightarrow> 
+lemma min_P0[simp]: "Rr (xs @ [0]) \<Longrightarrow> 
                    Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0"
 by(rule_tac Min_eqI, simp, simp, simp)
 
-lemma [intro]: "primerec rec_not (Suc 0)"
+lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)"
 apply(simp add: rec_not_def)
 apply(rule prime_cn, auto)
 apply(case_tac i, auto intro: prime_id)
@@ -825,24 +815,24 @@
 
 declare rec_maxr.simps[simp del] Maxr.simps[simp del] 
 declare le_lemma[simp]
-lemma [simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
+lemma min_with_suc3[simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
 by simp
 
 declare numeral_2_eq_2[simp]
 
-lemma [intro]: "primerec rec_disj (Suc (Suc 0))"
+lemma primerec_rec_disj_2[intro]: "primerec rec_disj (Suc (Suc 0))"
   apply(simp add: rec_disj_def, auto)
   apply(auto)
   apply(case_tac ia, auto intro: prime_id)
   done
 
-lemma [intro]: "primerec rec_less (Suc (Suc 0))"
+lemma primerec_rec_less_2[intro]: "primerec rec_less (Suc (Suc 0))"
   apply(simp add: rec_less_def, auto)
   apply(auto)
   apply(case_tac ia , auto intro: prime_id)
   done
 
-lemma [intro]: "primerec rec_eq (Suc (Suc 0))"
+lemma primerec_rec_eq_2[intro]: "primerec rec_eq (Suc (Suc 0))"
   apply(simp add: rec_eq_def)
   apply(rule_tac prime_cn, auto)
   apply(case_tac i, auto)
@@ -850,13 +840,13 @@
   apply(case_tac [!] i, auto intro: prime_id)
   done
 
-lemma [intro]: "primerec rec_le (Suc (Suc 0))"
+lemma primerec_rec_le_2[intro]: "primerec rec_le (Suc (Suc 0))"
   apply(simp add: rec_le_def)
   apply(rule_tac prime_cn, auto)
   apply(case_tac i, auto)
   done
 
-lemma [simp]:  
+lemma take_butlast_list_plus_two[simp]:  
   "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =  
                                                   ys @ [ys ! n]"
 apply(simp)
@@ -868,11 +858,11 @@
 lemma Maxr_Suc_simp: 
   "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
      else Maxr Rr xs w)"
-apply(auto simp: Maxr.simps Max.insert)
+apply(auto simp: Maxr.simps expand_conj_in_set)
 apply(rule_tac Max_eqI, auto)
 done
 
-lemma [simp]: "min (Suc n) n = n" by simp
+lemma min_Suc_1[simp]: "min (Suc n) n = n" by simp
 
 lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow> 
                               Sigma f (xs @ [n]) = 0"
@@ -880,7 +870,7 @@
 apply(simp add: Sigma_Suc_simp_rewrite)
 done
   
-lemma [elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
+lemma Sigma_Suc[elim]: "\<forall>k<Suc w. f (xs @ [k]) = Suc 0
         \<Longrightarrow> Sigma f (xs @ [w]) = Suc w"
 apply(induct w)
 apply(simp add: Sigma.simps, simp)
@@ -1058,28 +1048,23 @@
 text {*
   The following lemmas shows more directly the menaing of @{text "quo"}:
   *}
-lemma [elim!]: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
-proof(simp add: quo.simps Maxr.simps, auto,
-      rule_tac Max_eqI, simp, auto)
+lemma quo_is_div: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
+proof -
+  {
   fix xa ya
   assume h: "y * ya \<le> x"  "y > 0"
   hence "(y * ya) div y \<le> x div y"
     by(insert div_le_mono[of "y * ya" x y], simp)
-  from this and h show "ya \<le> x div y" by simp
-next
-  fix xa
-  show "y * (x div y) \<le> x"
-    apply(subgoal_tac "y * (x div y) + x mod y = x")
-    apply(rule_tac k = "x mod y" in add_leD1, simp)
-    apply(simp)
-    done
+  from this and h have "ya \<le> x div y" by simp}
+  thus ?thesis by(simp add: quo.simps Maxr.simps, auto,
+      rule_tac Max_eqI, simp, auto)
 qed
 
-lemma [intro]: "quo [x, 0] = 0"
+lemma quo_zero[intro]: "quo [x, 0] = 0"
 by(simp add: quo.simps Maxr.simps)
 
 lemma quo_div: "quo [x, y] = x div y"  
-by(case_tac "y=0", auto)
+by(case_tac "y=0", auto elim!:quo_is_div)
 
 text {*
   @{text "rec_noteq"} is the recursive function testing whether its
@@ -1120,13 +1105,13 @@
                            (0),id (Suc (Suc 0)) (Suc (0)), 
                                    id (Suc (Suc 0)) (0)]"
 
-lemma [intro]: "primerec rec_conj (Suc (Suc 0))"
+lemma primerec_rec_conj_2[intro]: "primerec rec_conj (Suc (Suc 0))"
   apply(simp add: rec_conj_def)
   apply(rule_tac prime_cn, auto)+
   apply(case_tac i, auto intro: prime_id)
   done
 
-lemma [intro]: "primerec rec_noteq (Suc (Suc 0))"
+lemma primerec_rec_noteq_2[intro]: "primerec rec_noteq (Suc (Suc 0))"
 apply(simp add: rec_noteq_def)
 apply(rule_tac prime_cn, auto)+
 apply(case_tac i, auto intro: prime_id)
@@ -1189,13 +1174,7 @@
   The correctness of @{text "rec_mod"}:
   *}
 lemma mod_lemma: "\<And> x y. rec_exec rec_mod [x, y] = (x mod y)"
-proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
-  fix x y
-  show "x - x div y * y = x mod (y::nat)"
-    using mod_div_equality2[of y x]
-    apply(subgoal_tac "y * (x div y) = (x div y ) * y", arith, simp)
-    done
-qed
+  by(simp add: rec_exec.simps rec_mod_def quo_lemma2 minus_div_mult_eq_mod)
 
 text{* lemmas for embranch function*}
 type_synonym ftype = "nat list \<Rightarrow> nat"
@@ -1604,7 +1583,7 @@
   "fac 0 = 1" |
   "fac (Suc x) = (Suc x) * fac x"
 
-lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
+lemma rec_exec_rec_dummyfac_0: "rec_exec rec_dummyfac [0, 0] = Suc 0"
 by(simp add: rec_dummyfac_def rec_exec.simps)
 
 lemma rec_cn_simp: "rec_exec (Cn n f gs) xs = 
@@ -1648,7 +1627,7 @@
   Cn 2 rec_prime [id 2 1]]
              in Cn 1 (rec_Minr Rr) [id 1 0, Cn 1 s [rec_fac]])"
 
-lemma [simp]: "n < Suc (n!)"
+lemma n_le_fact[simp]: "n < Suc (n!)"
 apply(induct n, simp)
 apply(simp add: fac.simps)
 apply(case_tac n, auto simp: fac.simps)
@@ -1667,7 +1646,7 @@
 apply(rule_tac x = u in exI, simp, auto)
 done
 
-lemma [intro]: "0 < n!"
+lemma fact_pos[intro]: "0 < n!"
 apply(induct n)
 apply(auto simp: fac.simps)
 done
@@ -1740,7 +1719,7 @@
   primerec (ys ! 0) n; primerec (ys ! 1) n\<rbrakk> \<Longrightarrow> primerec (ys ! i) n"
 by(case_tac i, auto)
 
-lemma [intro]: "primerec rec_prime (Suc 0)"
+lemma primerec_rec_prime_1[intro]: "primerec rec_prime (Suc 0)"
 apply(auto simp: rec_prime_def, auto)
 apply(rule_tac primerec_all_iff, auto, auto)
 apply(rule_tac primerec_all_iff, auto, auto simp:  
@@ -1835,7 +1814,7 @@
 
 declare lo.simps[simp del]
 
-lemma [elim]: "primerec rf n \<Longrightarrow> n > 0"
+lemma primerec_then_ge_0[elim]: "primerec rf n \<Longrightarrow> n > 0"
 apply(induct rule: primerec.induct, auto)
 done
 
@@ -1846,7 +1825,7 @@
 apply(auto, auto simp: nth_append)
 done
 
-lemma [intro!]:  "\<lbrakk>primerec rf n; n > 0\<rbrakk> \<Longrightarrow> primerec (rec_maxr rf) n"
+lemma primerec_rec_maxr[intro!]:  "\<lbrakk>primerec rf n; n > 0\<rbrakk> \<Longrightarrow> primerec (rec_maxr rf) n"
 apply(simp add: rec_maxr.simps)
 apply(rule_tac prime_cn, auto)
 apply(rule_tac primerec_all_iff, auto, auto simp: nth_append)
@@ -1859,23 +1838,10 @@
 apply(case_tac i, auto, case_tac nat, simp, simp add: numeral_2_eq_2)
 done
 
-lemma [intro]: "primerec rec_quo (Suc (Suc 0))"
-apply(simp add: rec_quo_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_mod (Suc (Suc 0))"
-apply(simp add: rec_mod_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_power (Suc (Suc 0))"
-apply(simp add: rec_power_def  numeral_2_eq_2 numeral_3_eq_3)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
+lemma primerec_2[intro]:
+"primerec rec_quo (Suc (Suc 0))" "primerec rec_mod (Suc (Suc 0))"
+"primerec rec_power (Suc (Suc 0))"
+  by(force simp: prime_cn prime_id rec_mod_def rec_quo_def rec_power_def prime_pr numeral)+
 
 text {*
   @{text "rec_lo"} is the recursive function used to implement @{text "Lo"}.
@@ -1919,14 +1885,12 @@
     done
 qed
 
-lemma [simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
+lemma MaxloR0[simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
 apply(rule_tac Max_eqI, auto simp: loR.simps)
 done
 
-lemma [simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
-apply(induct y, simp)
-apply(case_tac y, simp, simp)
-done
+lemma two_less_square[simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
+  by(induct y, auto)
 
 lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x"
 apply(case_tac y, simp, simp)
@@ -1942,17 +1906,16 @@
 lemma le_mult: "y \<noteq> (0::nat) \<Longrightarrow> x \<le> x * y"  
   by(induct y, simp, simp)
 
-lemma uplimit_loR:  "\<lbrakk>Suc 0 < x; Suc 0 < y; loR [x, y, xa]\<rbrakk> \<Longrightarrow> 
-  xa \<le> x"
-apply(simp add: loR.simps)
-apply(rule_tac classical, auto)
-apply(subgoal_tac "xa < y^xa")
-apply(subgoal_tac "y^xa \<le> y^xa * q", simp)
-apply(rule_tac le_mult, case_tac q, simp, simp)
-apply(rule_tac x_less_exp, simp)
-done
-
-lemma [simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
+lemma uplimit_loR:
+  assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]"
+  shows "xa \<le> x"
+proof -
+  have "Suc 0 < x \<Longrightarrow> Suc 0 < y \<Longrightarrow> y ^ xa dvd x \<Longrightarrow> xa \<le> x" 
+  by (meson Suc_lessD le_less_trans nat_dvd_not_less nat_le_linear x_less_exp)
+  thus ?thesis using assms by(auto simp: loR.simps)
+qed
+
+lemma loR_set_strengthen[simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
   {u. loR [x, y, u]} = {ya. ya \<le> x \<and> loR [x, y, ya]}"
 apply(rule_tac Collect_cong, auto)
 apply(erule_tac uplimit_loR, simp, simp)
@@ -2043,20 +2006,20 @@
     by simp
 qed
 
-lemma [simp]: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
+lemma lgR_ok: "\<lbrakk>Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow> xa \<le> x"
 apply(simp add: lgR.simps)
 apply(subgoal_tac "y^xa > xa", simp)
 apply(erule x_less_exp)
 done
 
-lemma [simp]: "\<lbrakk>Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow>
+lemma lgR_set_strengthen[simp]: "\<lbrakk>Suc 0 < x; Suc 0 < y; lgR [x, y, xa]\<rbrakk> \<Longrightarrow>
            {u. lgR [x, y, u]} =  {ya. ya \<le> x \<and> lgR [x, y, ya]}"
-apply(rule_tac Collect_cong, auto)
+apply(rule_tac Collect_cong, auto simp:lgR_ok)
 done
 
 lemma maxr_lg: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> Maxr lgR [x, y] x = lg x y"
 apply(simp add: lg.simps Maxr.simps, auto)
-apply(erule_tac x = xa in allE, simp)
+apply(erule_tac x = xa in allE, auto simp:lgR_ok)
 done
 
 lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
@@ -2445,7 +2408,7 @@
 apply(case_tac nat, auto simp: numeral_3_eq_3 numeral_4_eq_4)
 done
 
-lemma [intro]: "primerec rec_scan (Suc 0)"
+lemma primerec_rec_scan_1[intro]: "primerec rec_scan (Suc 0)"
 apply(auto simp: rec_scan_def, auto)
 done
 
@@ -2682,7 +2645,7 @@
     done
 qed
 
-lemma [elim]: 
+lemma nonempty_listE: 
   "Suc 0 \<le> length xs \<Longrightarrow> 
      (map ((\<lambda>a. rec_exec a (m # xs)) \<circ> 
          (\<lambda>i. recf.id (Suc (length xs)) (i))) 
@@ -2703,7 +2666,7 @@
   "(map ((\<lambda>a. rec_exec a (m # xs)) \<circ> 
           (\<lambda>i. recf.id (Suc (length xs)) (i))) 
             [Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs", simp)
-apply(auto, case_tac xs, auto)
+apply(auto elim:nonempty_listE, case_tac xs, auto)
 done
 
 definition rec_newconf:: "recf"
@@ -2878,180 +2841,135 @@
 lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0"
 by(induct f n rule: primerec.induct, auto)
 
-lemma [elim]: "primerec f 0 \<Longrightarrow> RR"
+lemma primerec_not0E[elim]: "primerec f 0 \<Longrightarrow> RR"
 apply(drule_tac primerec_not0, simp)
 done
 
-lemma [simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
-apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]", auto)
+lemma length_butlast[simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
+apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]",force)
 apply(rule_tac x = "last xs" in exI)
 apply(rule_tac x = "butlast xs" in exI)
 apply(case_tac "xs = []", auto)
 done
 
 text {*
-  The lemma relates the interpreter of primitive fucntions with
+  The lemma relates the interpreter of primitive functions with
   the calculation relation of general recursive functions. 
   *}
         
 declare numeral_2_eq_2[simp] numeral_3_eq_3[simp]
 
-lemma [intro]: "primerec rec_right (Suc 0)"
-apply(simp add: rec_right_def rec_lo_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]:  "primerec rec_pi (Suc 0)"
-apply(simp add: rec_pi_def rec_dummy_pi_def 
-                rec_np_def rec_fac_def rec_prime_def
-                rec_Minr.simps Let_def get_fstn_args.simps
-                arity.simps
-                rec_all.simps rec_sigma.simps rec_accum.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(simp add: rec_dummyfac_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
+lemma primerec_rec_right_1[intro]: "primerec rec_right (Suc 0)"
+  by(auto simp: rec_right_def rec_lo_def Let_def;force)
+
+lemma primerec_rec_pi_helper:
+  "\<forall>i<Suc (Suc 0). primerec ([recf.id (Suc 0) 0, recf.id (Suc 0) 0] ! i) (Suc 0)"
+  by fastforce
+
+lemmas primerec_rec_pi_helpers =
+  primerec_rec_pi_helper primerec_constn_1 primerec_rec_sg_1 primerec_rec_not_1 primerec_rec_conj_2
+
+lemma primrec_dummyfac:
+  "\<forall>i<Suc (Suc 0).
+       primerec
+        ([recf.id (Suc 0) 0,
+          Cn (Suc 0) s
+           [Cn (Suc 0) rec_dummyfac
+             [recf.id (Suc 0) 0, recf.id (Suc 0) 0]]] !
+         i)
+        (Suc 0)"
+  by(auto simp: rec_dummyfac_def;force)
+
+lemma primerec_rec_pi_1[intro]:  "primerec rec_pi (Suc 0)"
+  apply(simp add: rec_pi_def rec_dummy_pi_def 
+                  rec_np_def rec_fac_def rec_prime_def
+                  rec_Minr.simps Let_def get_fstn_args.simps
+                  arity.simps
+                  rec_all.simps rec_sigma.simps rec_accum.simps)
+  apply(tactic {* resolve_tac @{context} [@{thm prime_cn},  @{thm prime_pr}] 1*}
+       ;(simp add:primerec_rec_pi_helpers primrec_dummyfac)?)+
+  by fastforce+
+
+lemma primerec_rec_trpl[intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
+apply(simp add: rec_trpl_def)
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
     @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
 done
 
-lemma [intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
-apply(simp add: rec_trpl_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
+lemma primerec_rec_listsum2[intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
 apply(induct n)
 apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
     @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
 done
 
-lemma [elim]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
+lemma primerec_rec_strt': "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
 apply(induct n)
 apply(simp_all add: rec_strt'.simps Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
     @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)
 done
 
-lemma [elim]: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
+lemma primerec_rec_strt: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
 apply(simp add: rec_strt.simps rec_strt'.simps)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [elim]: 
+by(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt')
+
+lemma primerec_map_vl: 
   "i < vl \<Longrightarrow> primerec ((map (\<lambda>i. recf.id (Suc vl) (i)) 
         [Suc 0..<vl] @ [recf.id (Suc vl) (vl)]) ! i) (Suc vl)"
 apply(induct i, auto simp: nth_append)
 done
 
-lemma [intro]: "primerec rec_newleft0 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft1 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft2 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
-                rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft3 ((Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps rec_newleft0_def
+lemma primerec_recs[intro]:
+  "primerec rec_newleft0 (Suc (Suc 0))"
+  "primerec rec_newleft1 (Suc (Suc 0))"
+"primerec rec_newleft2 (Suc (Suc 0))"
+"primerec rec_newleft3 ((Suc (Suc 0)))"
+"primerec rec_newleft (Suc (Suc (Suc 0)))"
+"primerec rec_left (Suc 0)"
+"primerec rec_actn (Suc (Suc (Suc 0)))"
+"primerec rec_stat (Suc 0)"
+"primerec rec_newstat (Suc (Suc (Suc 0)))"
+apply(simp_all add: rec_newleft_def rec_embranch.simps rec_left_def rec_lo_def rec_entry_def
+                rec_actn_def Let_def arity.simps rec_newleft0_def rec_stat_def rec_newstat_def
                 rec_newleft1_def rec_newleft2_def rec_newleft3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newleft (Suc (Suc (Suc 0)))"
-apply(simp add: rec_newleft_def rec_embranch.simps 
-                Let_def arity.simps)
-apply(rule_tac prime_cn, auto+)
-done
-
-lemma [intro]: "primerec rec_left (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_actn (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def
-                Let_def rec_actn_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_stat (Suc 0)"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def Let_def 
-                rec_actn_def rec_stat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newstat (Suc (Suc (Suc 0)))"
-apply(simp add: rec_left_def rec_lo_def rec_entry_def 
-                Let_def rec_actn_def rec_stat_def rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))"
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*};force)+
+  done
+
+lemma primerec_rec_newrght[intro]: "primerec rec_newrght (Suc (Suc (Suc 0)))"
 apply(simp add: rec_newrght_def rec_embranch.simps
                 Let_def arity.simps rec_newrgt0_def 
                 rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "primerec rec_newconf (Suc (Suc 0))"
-apply(simp add: rec_newconf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
-apply(simp add: rec_inpt_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*};force)+
 done
 
-lemma [intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
-apply(simp add: rec_conf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-apply(auto simp: numeral_4_eq_4)
+lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))"
+apply(simp add: rec_newconf_def)
+by(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*};force)
+
+lemma primerec_rec_inpt[intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
+apply(simp add: rec_inpt_def)
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl)
 done
 
-lemma [intro]: "primerec rec_lg (Suc (Suc 0))"
-apply(simp add: rec_lg_def Let_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma [intro]:  "primerec rec_nonstop (Suc (Suc (Suc 0)))"
-apply(simp add: rec_nonstop_def rec_NSTD_def rec_stat_def
+lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
+apply(simp add: rec_conf_def)
+by(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral)
+
+lemma primerec_recs2[intro]:
+  "primerec rec_lg (Suc (Suc 0))"
+  "primerec rec_nonstop (Suc (Suc (Suc 0)))"
+apply(simp_all add: rec_lg_def rec_nonstop_def rec_NSTD_def rec_stat_def
      rec_lo_def Let_def rec_left_def rec_right_def rec_newconf_def
      rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn}, 
-    @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
+by(tactic {* resolve_tac @{context} [@{thm prime_cn}, 
+    @{thm prime_id}, @{thm prime_pr}] 1*};fastforce)+
 
 lemma primerec_terminate: 
   "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
@@ -3087,9 +3005,7 @@
   and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs"
   and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m"
   have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
-    using h
-    apply(auto) 
-    by(rule_tac ind2, simp)
+    using h ind2 by(auto)
   moreover have "terminate f (butlast xs)"
     using ind1[of "butlast xs"] h
     by simp
@@ -3128,20 +3044,12 @@
   The correctness of @{text "rec_valu"}.
 *}
 lemma value_lemma: "rec_exec rec_valu [r] = valu r"
-apply(simp add: rec_exec.simps rec_valu_def lg_lemma)
-done
-
-lemma [intro]: "primerec rec_valu (Suc 0)"
-apply(simp add: rec_valu_def)
-apply(rule_tac k = "Suc (Suc 0)" in prime_cn)
-apply(auto simp: prime_s)
-proof -
-  show "primerec rec_lg (Suc (Suc 0))" by auto
-next
-  show "Suc (Suc 0) = Suc (Suc 0)" by simp
-next
-  show "primerec (constn (Suc (Suc 0))) (Suc 0)" by auto
-qed
+  by(simp add: rec_exec.simps rec_valu_def lg_lemma)
+
+lemma primerec_rec_valu_1[intro]: "primerec rec_valu (Suc 0)"
+  unfolding rec_valu_def
+  apply(rule prime_cn[of _ "Suc (Suc 0)"])
+  by auto auto
 
 declare valu.simps[simp del]
 
@@ -3153,14 +3061,14 @@
   "rec_F = Cn (Suc (Suc 0)) rec_valu [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])]]"
 
-lemma get_fstn_args_nth: 
+lemma get_fstn_args_nth[simp]: 
   "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
 apply(induct n, simp)
 apply(case_tac "k = n", simp_all add: get_fstn_args.simps 
                                       nth_append)
 done
 
-lemma [simp]: 
+lemma get_fstn_args_is_id[simp]: 
   "\<lbrakk>ys \<noteq> [];
   k < length ys\<rbrakk> \<Longrightarrow>
   (get_fstn_args (length ys) (length ys) ! k) = 
@@ -3268,9 +3176,9 @@
 
 subsection {* Relating interperter functions to the execution of TMs *}
 
-lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
+lemma bl2wc_0[simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
+
+lemma fetch_action_map_4[simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
 apply(simp add: fetch.simps)
 done
 
@@ -3295,7 +3203,7 @@
 
 declare godel_code.simps[simp del]
 
-lemma [simp]: "0 < godel_code' nl n"
+lemma godel_code'_nonzero[simp]: "0 < godel_code' nl n"
 apply(induct nl arbitrary: n)
 apply(auto simp: godel_code'.simps)
 done
@@ -3308,14 +3216,14 @@
 apply(auto simp: godel_code.simps)
 done
 
-lemma [elim]: 
+lemma godel_code_1_iff[elim]: 
   "\<lbrakk>i < length nl; \<not> Suc 0 < godel_code nl\<rbrakk> \<Longrightarrow> nl ! i = 0"
 using godel_code_great[of nl] godel_code_eq_1[of nl]
 apply(simp)
 done
 
 lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
-proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
+proof (simp only: Prime.simps coprime_def, auto simp: dvd_def,
       rule_tac classical, simp)
   fix d k ka
   assume case_ka: "\<forall>u<d * ka. \<forall>v<d * ka. u * v \<noteq> d * ka" 
@@ -3323,10 +3231,7 @@
     and h: "(0::nat) < d" "d \<noteq> Suc 0" "Suc 0 < d * ka" 
            "ka \<noteq> k" "Suc 0 < d * k"
   from h have "k > Suc 0 \<or> ka >Suc 0"
-    apply(auto)
-    apply(case_tac ka, simp, simp)
-    apply(case_tac k, simp, simp)
-    done
+    by (cases ka;cases k;force+)
   from this show "False"
   proof(erule_tac disjE)
     assume  "(Suc 0::nat) < k"
@@ -3402,7 +3307,7 @@
 apply(simp)
 done
 
-lemma [intro]: "Prime (Suc (Suc 0))"
+lemma prime_2[intro]: "Prime (Suc (Suc 0))"
 apply(auto simp: Prime.simps)
 apply(case_tac u, simp, case_tac nat, simp, simp)
 done
@@ -3431,15 +3336,10 @@
 done
 
 lemma Pi_power_coprime: "i \<noteq> j \<Longrightarrow> coprime ((Pi i)^m) ((Pi j)^n)"
-by(rule_tac coprime_exp2_nat, erule_tac Pi_coprime)
+  unfolding coprime_power_right_iff coprime_power_left_iff using Pi_coprime by auto
 
 lemma coprime_dvd_mult_nat2: "\<lbrakk>coprime (k::nat) n; k dvd n * m\<rbrakk> \<Longrightarrow> k dvd m"
-apply(erule_tac coprime_dvd_mult_nat)
-apply(simp add: dvd_def, auto)
-apply(rule_tac x = ka in exI)
-apply(subgoal_tac "n * m = m * n", simp)
-apply(simp add: nat_mult_commute)
-done
+  unfolding coprime_dvd_mult_right_iff.
 
 declare godel_code'.simps[simp del]
 
@@ -3504,7 +3404,7 @@
 
 lemma Pi_coprime_pre: 
   "length ps \<le> i \<Longrightarrow> coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
+proof(induct "length ps" arbitrary: ps)
   fix x ps
   assume ind: 
     "\<And>ps. \<lbrakk>x = length ps; length ps \<le> i\<rbrakk> \<Longrightarrow>
@@ -3518,20 +3418,19 @@
          godel_code' (butlast ps) (Suc 0) * Pi (length ps)^(last ps)"
     using godel_code'_butlast_last_id[of ps 0] h 
     by(case_tac ps, simp, simp)
-  from g have 
+  from g have "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
+    unfolding coprime_power_right_iff using Pi_coprime h(2) by auto
+   with g have 
     "coprime (Pi (Suc i)) (godel_code' (butlast ps) (Suc 0) *
                                         Pi (length ps)^(last ps)) "
-  proof(rule_tac coprime_mult_nat, simp)
-    show "coprime (Pi (Suc i)) (Pi (length ps) ^ last ps)"
-      apply(rule_tac coprime_exp_nat, rule prime_coprime, auto)
-      using Pi_notEq[of "Suc i" "length ps"] h by simp
-  qed
+    unfolding coprime_mult_right_iff coprime_power_right_iff by auto
+
   from this and k show "coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
     by simp
-qed
+qed (auto simp add: godel_code'.simps)
 
 lemma Pi_coprime_suf: "i < j \<Longrightarrow> coprime (Pi i) (godel_code' ps j)"
-proof(induct "length ps" arbitrary: ps, simp add: godel_code'.simps)
+proof(induct "length ps" arbitrary: ps)
   fix x ps
   assume ind: 
     "\<And>ps. \<lbrakk>x = length ps; i < j\<rbrakk> \<Longrightarrow> 
@@ -3547,13 +3446,11 @@
   from g have
     "coprime (Pi i) (godel_code' (butlast ps) j * 
                           Pi (length ps + j - 1)^last ps)"
-    apply(rule_tac coprime_mult_nat, simp)
-    using  Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
-    apply(auto)
-    done
+    using Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
+    by(auto)
   from k and this show "coprime (Pi i) (godel_code' ps j)"
     by auto
-qed
+qed (simp add: godel_code'.simps)
 
 lemma godel_finite: 
   "finite {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
@@ -3619,26 +3516,14 @@
     assume mult_dvd: 
       "Pi (Suc i) ^ y dvd ?pref *  Pi (Suc i) ^ nl ! i * ?suf'"
     hence "Pi (Suc i) ^ y dvd ?pref * Pi (Suc i) ^ nl ! i"
-    proof(rule_tac coprime_dvd_mult_nat)
-      show "coprime (Pi (Suc i)^y) ?suf'"
-      proof -
-        have "coprime (Pi (Suc i) ^ y) (?suf'^(Suc 0))"
-          apply(rule_tac coprime_exp2_nat)
-          apply(rule_tac  Pi_coprime_suf, simp)
-          done
-        thus "?thesis" by simp
-      qed
+    proof -
+      have "coprime (Pi (Suc i)^y) ?suf'" by (simp add: Pi_coprime_suf)
+      thus ?thesis using coprime_dvd_mult_left_iff mult_dvd by blast
     qed
     hence "Pi (Suc i) ^ y dvd Pi (Suc i) ^ nl ! i"
     proof(rule_tac coprime_dvd_mult_nat2)
-      show "coprime (Pi (Suc i) ^ y) ?pref"
-      proof -
-        have "coprime (Pi (Suc i)^y) (?pref^Suc 0)"
-          apply(rule_tac coprime_exp2_nat)
-          apply(rule_tac Pi_coprime_pre, simp)
-          done
-        thus "?thesis" by simp
-      qed
+      have "coprime (Pi (Suc i)^y) (?pref^Suc 0)" using Pi_coprime_pre by simp
+      thus "coprime (Pi (Suc i) ^ y) ?pref" by simp
     qed
     hence "Pi (Suc i) ^ y \<le>  Pi (Suc i) ^ nl ! i "
       apply(rule_tac dvd_imp_le, auto)
@@ -3654,7 +3539,7 @@
     by(rule_tac godel_code_in, simp)
 qed
 
-lemma [simp]: 
+lemma godel_code'_set[simp]: 
   "{u. Pi (Suc i) ^ u dvd (Suc (Suc 0)) ^ length nl * 
                                      godel_code' nl (Suc 0)} = 
     {u. Pi (Suc i) ^ u dvd  godel_code' nl (Suc 0)}"
@@ -3662,17 +3547,9 @@
 apply(rule_tac n = " (Suc (Suc 0)) ^ length nl" in 
                                  coprime_dvd_mult_nat2)
 proof -
-  fix u
-  show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)"
-  proof(rule_tac coprime_exp2_nat)
-    have "Pi 0 = (2::nat)"
-      apply(simp add: Pi.simps)
-      done
-    moreover have "coprime (Pi (Suc i)) (Pi 0)"
-      apply(rule_tac Pi_coprime, simp)
-      done
-    ultimately show "coprime (Pi (Suc i)) (Suc (Suc 0))" by simp
-  qed
+  have "Pi 0 = (2::nat)" by(simp add: Pi.simps)
+  show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)" for u
+    using Pi_coprime Pi.simps(1) by force
 qed
   
 lemma godel_code_get_nth: 
@@ -3680,10 +3557,6 @@
            Max {u. Pi (Suc i) ^ u dvd godel_code nl} = nl ! i"
 by(simp add: godel_code.simps godel_code'_get_nth)
 
-lemma "trpl l st r = godel_code' [l, st, r] 0"
-apply(simp add: trpl.simps godel_code'.simps)
-done
-
 lemma mod_dvd_simp: "(x mod y = (0::nat)) = (y dvd x)"
 by(simp add: dvd_def, auto)
 
@@ -3694,10 +3567,10 @@
 done
 
 
-lemma [elim]: "Pi n = 0 \<Longrightarrow> RR"
+lemma Pi_nonzeroE[elim]: "Pi n = 0 \<Longrightarrow> RR"
   using Pi_not_0[of n] by simp
 
-lemma [elim]: "Pi n = Suc 0 \<Longrightarrow> RR"
+lemma Pi_not_oneE[elim]: "Pi n = Suc 0 \<Longrightarrow> RR"
   using Pi_gr_1[of n] by simp
 
 lemma finite_power_dvd:
@@ -3725,15 +3598,9 @@
     have "Pi m ^ y dvd Pi m ^ l"
     proof -
       have "Pi m ^ y dvd Pi m ^ l * Pi n ^ st"
-        using h g
-        apply(rule_tac n = "Pi k^r" in coprime_dvd_mult_nat)
-        apply(rule Pi_power_coprime, simp, simp)
-        done
-      thus "Pi m^y dvd Pi m^l"
-        apply(rule_tac n = " Pi n ^ st" in coprime_dvd_mult_nat)
-        using g
-        apply(rule_tac Pi_power_coprime, simp, simp)
-        done
+        using h g Pi_power_coprime
+        by (simp add: coprime_dvd_mult_left_iff)
+      thus "Pi m^y dvd Pi m^l" using g Pi_power_coprime coprime_dvd_mult_left_iff by blast
     qed
     thus "y \<le> (l::nat)"
       apply(rule_tac a = "Pi m" in power_le_imp_le_exp)
@@ -3751,7 +3618,7 @@
 apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto)
 done
 
-lemma [simp]: "left (trpl l st r) = l"
+lemma left_trpl_fst[simp]: "left (trpl l st r) = l"
 apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp)
 apply(auto simp: conf_decode1)
 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r")
@@ -3759,7 +3626,7 @@
 apply(erule_tac x = l in allE, auto)
 done   
 
-lemma [simp]: "stat (trpl l st r) = st"
+lemma stat_trpl_snd[simp]: "stat (trpl l st r) = st"
 apply(simp add: stat.simps trpl.simps lo.simps 
                 loR.simps mod_dvd_simp, auto)
 apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
@@ -3770,7 +3637,7 @@
 apply(erule_tac x = st in allE, auto)
 done
 
-lemma [simp]: "rght (trpl l st r) = r"
+lemma rght_trpl_trd[simp]: "rght (trpl l st r) = r"
 apply(simp add: rght.simps trpl.simps lo.simps 
                 loR.simps mod_dvd_simp, auto)
 apply(subgoal_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r
@@ -3938,7 +3805,7 @@
     by simp
 qed
 
-lemma [simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
+lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
 by(simp add: fetch.simps)
 
 lemma Five_Suc: "5 = Suc 4" by simp
@@ -4029,11 +3896,11 @@
 qed
 
 
-lemma [intro!]: 
+lemma tpl_eqI[intro!]: 
   "\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> trpl a b c = trpl a' b' c'"
 by simp
 
-lemma [simp]: "bl2wc [Bk] = 0"
+lemma bl2wc_Bk[simp]: "bl2wc [Bk] = 0"
 by(simp add: bl2wc.simps bl2nat.simps)
 
 lemma bl2nat_double: "bl2nat xs (Suc n) = 2 * bl2nat xs n"
@@ -4058,45 +3925,17 @@
 qed
 
 
-lemma [simp]: "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
-apply(case_tac c, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]:
+lemma bl2wc_simps[simp]:
   "bl2wc (Oc # tl c) = Suc (bl2wc c) - bl2wc c mod 2 "
-apply(case_tac c, case_tac [2] a, simp)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc (Bk # c) = 2*bl2wc (c)"
-apply(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "bl2wc [Oc] = Suc 0"
- by(simp add: bl2wc.simps bl2nat.simps)
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc (tl b) = bl2wc b div 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "b \<noteq> [] \<Longrightarrow> bl2wc ([hd b]) = bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: "\<lbrakk>b \<noteq> []\<rbrakk> \<Longrightarrow> bl2wc (hd b # c) = 2 * bl2wc c + bl2wc b mod 2"
-apply(case_tac b, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-
-lemma [simp]: " 2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2" 
-  by(simp add: mult_div_cancel)
-
-lemma [simp]: "bl2wc (Oc # list) mod 2 = Suc 0" 
-  by(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
-
+  "bl2wc (Bk # c) = 2*bl2wc (c)"
+  "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
+  "bl2wc [Oc] = Suc 0"
+  "c \<noteq> [] \<Longrightarrow> bl2wc (tl c) = bl2wc c div 2"
+  "c \<noteq> [] \<Longrightarrow> bl2wc [hd c] = bl2wc c mod 2"
+  "c \<noteq> [] \<Longrightarrow> bl2wc (hd c # d) = 2 * bl2wc d + bl2wc c mod 2"
+  "2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2"
+  "bl2wc (Oc # list) mod 2 = Suc 0" 
+  by(cases c;cases "hd c";force simp: bl2wc.simps bl2nat.simps bl2nat_double)+
 
 declare code.simps[simp del]
 declare nth_of.simps[simp del]
@@ -4136,21 +3975,15 @@
     done
 qed
 
-lemma [simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
-apply(induct x)
-apply(simp add: bl2nat.simps)
-apply(simp add: bl2nat.simps bl2nat_double exp_ind)
-done
-
-lemma [simp]: "bl2nat (Oc\<up>y) 0 = 2^y - Suc 0"
+lemma bl2nat_simps[simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
+  "bl2nat (Bk\<up>x) n = 0"
+ by(induct x;force simp: bl2nat.simps bl2nat_double exp_ind)+
+
+lemma bl2nat_exp_zero[simp]: "bl2nat (Oc\<up>y) 0 = 2^y - Suc 0"
 apply(induct y, auto simp: bl2nat.simps bl2nat_double)
 apply(case_tac "(2::nat)^y", auto)
 done
 
-lemma [simp]: "bl2nat (Bk\<up>l) n = 0"
-apply(induct l, auto simp: bl2nat.simps bl2nat_double exp_ind)
-done
-
 lemma bl2nat_cons_bk: "bl2nat (ks @ [Bk]) 0 = bl2nat ks 0"
 apply(induct ks, auto simp: bl2nat.simps)
 apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
@@ -4200,9 +4033,8 @@
 lemma tape_of_nat_list_butlast_last:
   "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"
 apply(induct ys, simp, simp)
-apply(case_tac "ys = []", simp add: tape_of_nl_abv tape_of_nat_abv
-                                    tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_cons tape_of_nat_abv)
+apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def)
+apply(simp add: tape_of_nl_cons tape_of_nat_def)
 done
 
 lemma listsum2_append:
@@ -4244,8 +4076,8 @@
   thus "length (<xs @ [x]>) =
     Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
     apply(case_tac "xs = []")
-    apply(simp add: tape_of_nl_abv listsum2.simps 
-      tape_of_nat_list.simps tape_of_nat_abv)
+    apply(simp add: tape_of_list_def listsum2.simps 
+      tape_of_nat_list.simps tape_of_nat_def)
     apply(simp add: tape_of_nat_list_butlast_last)
     using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
     apply(simp)
@@ -4267,7 +4099,7 @@
   apply(simp)
   done
 
-lemma [simp]:
+lemma trpl_code_simp[simp]:
  "trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) = 
     rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
 apply(simp add: steps.simps rec_exec.simps conf_lemma  conf.simps 
@@ -4354,12 +4186,12 @@
   qed
 qed
 
-lemma [simp]: "bl2wc (Bk\<up> m) = 0"
+lemma bl2wc_Bk_0[simp]: "bl2wc (Bk\<up> m) = 0"
 apply(induct m)
 apply(simp, simp)
 done
 
-lemma [simp]: "bl2wc (Oc\<up> rs@Bk\<up> n) = bl2wc (Oc\<up> rs)"
+lemma bl2wc_Oc_then_Bk[simp]: "bl2wc (Oc\<up> rs@Bk\<up> n) = bl2wc (Oc\<up> rs)"
 apply(induct rs, simp, 
   simp add: bl2wc.simps bl2nat.simps bl2nat_double)
 done
@@ -4438,10 +4270,10 @@
   qed
 qed
 
-lemma [simp]: "actn m 0 r = 4"
+lemma actn_0_is_4[simp]: "actn m 0 r = 4"
 by(simp add: actn.simps)
 
-lemma [simp]: "newstat m 0 r = 0"
+lemma newstat_0_0[simp]: "newstat m 0 r = 0"
 by(simp add: newstat.simps)
 
 declare step_red[simp del]
@@ -4536,7 +4368,7 @@
 apply(auto)
 done
 
-lemma [elim]: "x > Suc 0 \<Longrightarrow> Max {u. x ^ u dvd x ^ r} = r"
+lemma max_divisors: "x > Suc 0 \<Longrightarrow> Max {u. x ^ u dvd x ^ r} = r"
 proof(rule_tac Max_eqI)
   assume "x > Suc 0"
   thus "finite {u. x ^ u dvd x ^ r}"
@@ -4555,10 +4387,16 @@
   show "r \<in> {u. x ^ u dvd x ^ r}" by simp
 qed  
 
-lemma lo_power: "x > Suc 0 \<Longrightarrow> lo (x ^ r) x = r"
-apply(auto simp: lo.simps loR.simps mod_dvd_simp)
-apply(case_tac "x^r", simp_all)
-done
+lemma lo_power:
+  assumes "x > Suc 0" shows "lo (x ^ r) x = r"
+proof -
+  have "\<not> Suc 0 < x ^ r \<Longrightarrow> r = 0" using assms
+    by (metis Suc_lessD Suc_lessI nat_power_eq_Suc_0_iff zero_less_power)
+  moreover have "\<forall>xa. \<not> x ^ xa dvd x ^ r \<Longrightarrow> r = 0"
+    using dvd_refl assms by(cases "x^r";blast)
+  ultimately show ?thesis using assms
+    by(auto simp: lo.simps loR.simps mod_dvd_simp elim:max_divisors)
+qed
 
 lemma lo_rgt: "lo (trpl 0 0 r) (Pi 2) = r"
 apply(simp add: trpl.simps lo_power)