tm: comparison thys/UF.thy

equal deleted inserted replaced

-:d5a0e25c4742
+:a9003e6d0463
 (* Title: thys/UF.thy
 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 {*
 This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined
 in terms of recursive functions. This @{text "rec_F"} is essentially an
 declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
 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)
 lemma rec_pr_0_simp_rewrite_single_param: "
 case (Suc n) thus "?case"
 by(simp add: get_fstn_args.simps rec_exec.simps
 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)
 done
 apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<le> x")
 apply(erule_tac order_trans, simp)
 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"
+lemma Minr_strip_Suc[simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"
-apply(simp add: Minr.simps, auto)
+by(cases "\<forall>x\<le>w. \<not> Rr (xs @ [x])",auto simp add: Minr.simps expand_conj_in_set)
-apply(case_tac "\<forall>x\<le>w. \<not> Rr (xs @ [x])", auto)
-done
+lemma x_empty_set[simp]: "\<forall>x\<le>w. \<not> Rr (xs @ [x]) \<Longrightarrow>
-lemma [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)
 apply(rule_tac Min_in, auto)
 done
 lemma min_Suc_Suc[simp]: "min (Suc (Suc x)) x = x"
 by auto
 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"
+lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
-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"
 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)
 apply(case_tac i, auto intro: prime_id)
 apply(auto simp: nth_append)
 primerec (rec_all rt rf) n"
 apply(simp add: rec_all.simps, auto)
 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)
 done
 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @
 [id vl (vl - 1)]))"
 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)
 apply(case_tac ia, auto)
 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)
 apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
 done
 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"
 apply(induct n, simp add: Sigma.simps)
 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)
 apply(simp add: Sigma.simps)
 done
 declare quo.simps[simp del]
 text {*
 The following lemmas shows more directly the menaing of @{text "quo"}:
 *}
-lemma [elim!]: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
+lemma quo_is_div: "y > 0 \<Longrightarrow> quo [x, y] = x div y"
-proof(simp add: quo.simps Maxr.simps, auto,
+proof -
-rule_tac Max_eqI, simp, auto)
+{
 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
+from this and h have "ya \<le> x div y" by simp}
-next
+thus ?thesis by(simp add: quo.simps Maxr.simps, auto,
-fix xa
+rule_tac Max_eqI, simp, auto)
-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
 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
 two arguments are not equal.
 *}
 [id (Suc (Suc (Suc 0))) (0)]]]
 in Cn (Suc (Suc 0)) (rec_maxr rR)) [id (Suc (Suc 0))
 (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)
 done
 text {*
 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)
+by(simp add: rec_exec.simps rec_mod_def quo_lemma2 minus_div_mult_eq_mod)
-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
 text{* lemmas for embranch function*}
 type_synonym ftype = "nat list \<Rightarrow> nat"
 type_synonym rtype = "nat list \<Rightarrow> bool"
 fun fac :: "nat \<Rightarrow> nat"  ("_!" [100] 99)
 where
 "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 =
 (let rgs = map (\<lambda> g. rec_exec g xs) gs in
 rec_exec f rgs)"
 where
 "rec_np = (let Rr = Cn 2 rec_conj [Cn 2 rec_less [id 2 0, id 2 1],
 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)
 done
 apply(erule_tac x = u in allE, simp)
 apply(case_tac "Prime u", simp)
 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
 lemma fac_Suc: "Suc n! =  (Suc n) * (n!)" by(simp add: fac.simps)
 lemma Suc_Suc_induct[elim!]: "\<lbrakk>i < Suc (Suc 0);
 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:
 numeral_2_eq_2 numeral_3_eq_3)
 done
 "lo x y  = (if x > 1 \<and> y > 1 \<and> {u. loR [x, y, u]} \<noteq> {} then Max {u. loR [x, y, u]}
 else 0)"
 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
 lemma primerec_sigma[intro!]:
 "\<lbrakk>n > Suc 0; primerec rf n\<rbrakk> \<Longrightarrow>
 primerec (rec_sigma rf) n"
 apply(simp add: rec_sigma.simps)
 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)
 done
 primerec (ys ! 1) n;
 primerec (ys ! 2) n\<rbrakk> \<Longrightarrow> primerec (ys ! i) n"
 apply(case_tac i, auto, case_tac nat, simp, simp add: numeral_2_eq_2)
 done
-lemma [intro]: "primerec rec_quo (Suc (Suc 0))"
+lemma primerec_2[intro]:
-apply(simp add: rec_quo_def)
+"primerec rec_quo (Suc (Suc 0))" "primerec rec_mod (Suc (Suc 0))"
-apply(tactic {* resolve_tac [@{thm prime_cn},
+"primerec rec_power (Suc (Suc 0))"
-@{thm prime_id}] 1*}, auto+)+
+by(force simp: prime_cn prime_id rec_mod_def rec_quo_def rec_power_def prime_pr numeral)+
-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
 text {*
 @{text "rec_lo"} is the recursive function used to implement @{text "Lo"}.
 *}
 definition rec_lo :: "recf"
 Maxr loR [x, y] x"
 apply(simp)
 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"
+lemma two_less_square[simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
-apply(induct y, simp)
+by(induct y, auto)
-apply(case_tac y, simp, simp)
-done
 lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x"
 apply(case_tac y, simp, simp)
 done
 done
 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>
+lemma uplimit_loR:
-xa \<le> x"
+assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]"
-apply(simp add: loR.simps)
+shows "xa \<le> x"
-apply(rule_tac classical, auto)
+proof -
-apply(subgoal_tac "xa < y^xa")
+have "Suc 0 < x \<Longrightarrow> Suc 0 < y \<Longrightarrow> y ^ xa dvd x \<Longrightarrow> xa \<le> x"
-apply(subgoal_tac "y^xa \<le> y^xa * q", simp)
+by (meson Suc_lessD le_less_trans nat_dvd_not_less nat_le_linear x_less_exp)
-apply(rule_tac le_mult, case_tac q, simp, simp)
+thus ?thesis using assms by(auto simp: loR.simps)
-apply(rule_tac x_less_exp, simp)
+qed
-done
+lemma loR_set_strengthen[simp]: "\<lbrakk>xa \<le> x; loR [x, y, xa]; Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
-lemma [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)
 done
 done
 ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
 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"
 apply(simp add: maxr_lg lg_maxr)
 done
 apply(case_tac nat, auto)
 apply(case_tac nata, auto simp: numeral_2_eq_2)
 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
 text {*
 The correctness of @{text "rec_newrght"}.
 rule_tac x = "last xs" in exI)
 apply(case_tac "xs \<noteq> []", auto)
 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)))
 [Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs"
 using map_cons_eq[of m xs]
 trpl_lemma inpt.simps strt_lemma)
 apply(subgoal_tac
 "(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"
 where
 "rec_newconf =
 declare nonstop.simps[simp del]
 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"
+lemma length_butlast[simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
-apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]", auto)
+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)"
+lemma primerec_rec_right_1[intro]: "primerec rec_right (Suc 0)"
-apply(simp add: rec_right_def rec_lo_def Let_def)
+by(auto simp: rec_right_def rec_lo_def Let_def;force)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+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_pi (Suc 0)"
+lemma primerec_rec_listsum2[intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
-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},
-@{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"
 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},
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt')
-done
+lemma primerec_map_vl:
-lemma [elim]:
 "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)))"
+lemma primerec_recs[intro]:
-apply(simp add: rec_newleft_def rec_embranch.simps
+"primerec rec_newleft0 (Suc (Suc 0))"
-Let_def arity.simps rec_newleft0_def
+"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},
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*};force)+
 done
-lemma [intro]: "primerec rec_newleft1 ((Suc (Suc 0)))"
+lemma primerec_rec_newrght[intro]: "primerec rec_newrght (Suc (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
-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(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},
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*};force)+
 done
-lemma [intro]: "primerec rec_newconf (Suc (Suc 0))"
+lemma primerec_rec_newconf[intro]: "primerec rec_newconf (Suc (Suc 0))"
 apply(simp add: rec_newconf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*};force)
-done
+lemma primerec_rec_inpt[intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
-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},
+apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl)
 done
-lemma [intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
+lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
 apply(simp add: rec_conf_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*};force simp: numeral)
-apply(auto simp: numeral_4_eq_4)
-done
+lemma primerec_recs2[intro]:
+"primerec rec_lg (Suc (Suc 0))"
-lemma [intro]: "primerec rec_lg (Suc (Suc 0))"
+"primerec rec_nonstop (Suc (Suc (Suc 0)))"
-apply(simp add: rec_lg_def Let_def)
+apply(simp_all add: rec_lg_def rec_nonstop_def rec_NSTD_def rec_stat_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
 rec_lo_def Let_def rec_left_def rec_right_def rec_newconf_def
 rec_newstat_def)
-apply(tactic {* resolve_tac [@{thm prime_cn},
+by(tactic {* resolve_tac @{context} [@{thm prime_cn},
-@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
+@{thm prime_id}, @{thm prime_pr}] 1*};fastforce)+
-done
 lemma primerec_terminate:
 "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
 proof(induct arbitrary: xs rule: primerec.induct)
 fix xs
 fix f n g m xs
 assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs"
 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
+using h ind2 by(auto)
-apply(auto)
-by(rule_tac ind2, simp)
 moreover have "terminate f (butlast xs)"
 using ind1[of "butlast xs"] h
 by simp
 moreover have "length (butlast xs) = n"
 using h by simp
 text {*
 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)
+by(simp add: rec_exec.simps rec_valu_def lg_lemma)
-done
+lemma primerec_rec_valu_1[intro]: "primerec rec_valu (Suc 0)"
-lemma [intro]: "primerec rec_valu (Suc 0)"
+unfolding rec_valu_def
-apply(simp add: rec_valu_def)
+apply(rule prime_cn[of _ "Suc (Suc 0)"])
-apply(rule_tac k = "Suc (Suc 0)" in prime_cn)
+by auto auto
-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
 declare valu.simps[simp del]
 text {*
 The definition of the universal function @{text "rec_F"}.
 definition rec_F :: "recf"
 where
 "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) =
 id (length ys) (k)"
 by(erule_tac get_fstn_args_nth)
 "code tp = (let nl = modify_tprog tp in
 godel_code nl)"
 subsection {* Relating interperter functions to the execution of TMs *}
-lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
+lemma bl2wc_0[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 fetch_action_map_4[simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
 apply(simp add: fetch.simps)
 done
 lemma Pi_gr_1[simp]: "Pi n > Suc 0"
 proof(induct n, auto simp: Pi.simps Np.simps)
 using Pi_gr_1[of n]
 by arith
 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
 lemma godel_code_great: "godel_code nl > 0"
 lemma godel_code_eq_1: "(godel_code nl = 1) = (nl = [])"
 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"
 and case_k: "\<forall>u<d * k. \<forall>v<d * k. u * v \<noteq> d * k"
 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)
+by (cases ka;cases k;force+)
-apply(case_tac ka, simp, simp)
-apply(case_tac k, simp, simp)
-done
 from this show "False"
 proof(erule_tac disjE)
 assume  "(Suc 0::nat) < k"
 hence "k < d*k \<and> d < d*k"
 using h
 apply(simp)
 using Pi_inc_gr[of j i]
 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
 lemma Prime_Pi[intro]: "Prime (Pi n)"
 using Prime_Pi[of j]
 apply(rule_tac prime_coprime, simp_all add: Pi_notEq)
 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)
+unfolding coprime_dvd_mult_right_iff.
-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
 declare godel_code'.simps[simp del]
 lemma godel_code'_butlast_last_id' :
 "godel_code' (ys @ [y]) (Suc j) = godel_code' ys (Suc j) *
 done
 qed
 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>
 coprime (Pi (Suc i)) (godel_code' ps (Suc 0))"
 and h: "Suc x = length ps"
 using h by auto
 have k: "godel_code' ps (Suc 0) =
 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)
+unfolding coprime_mult_right_iff coprime_power_right_iff by auto
-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
 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>
 coprime (Pi i) (godel_code' ps j)"
 and h: "Suc x = length (ps::nat list)" "i < j"
 apply(case_tac "ps = []", simp, simp)
 done
 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
-using  Pi_power_coprime[of i "length ps + j - 1" 1 "last ps"] h
+by(auto)
-apply(auto)
-done
 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)}"
 proof(rule_tac n = "godel_code' nl (Suc 0)" in
 bounded_nat_set_is_finite, auto,
 proof(simp)
 let ?suf' = "godel_code' (drop (Suc i) nl) (Suc (Suc i))"
 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)
+proof -
-show "coprime (Pi (Suc i)^y) ?suf'"
+have "coprime (Pi (Suc i)^y) ?suf'" by (simp add: Pi_coprime_suf)
-proof -
+thus ?thesis using coprime_dvd_mult_left_iff mult_dvd by blast
-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
 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"
+have "coprime (Pi (Suc i)^y) (?pref^Suc 0)" using Pi_coprime_pre by simp
-proof -
+thus "coprime (Pi (Suc i) ^ y) ?pref" by simp
-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
 qed
 hence "Pi (Suc i) ^ y \<le>  Pi (Suc i) ^ nl ! i "
 apply(rule_tac dvd_imp_le, auto)
 done
 thus "y \<le> nl ! i"
 thus "nl ! i \<in> {u. Pi (Suc i) ^ u dvd godel_code' nl (Suc 0)}"
 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)}"
 apply(rule_tac Collect_cong, auto)
 apply(rule_tac n = " (Suc (Suc 0)) ^ length nl" in
 coprime_dvd_mult_nat2)
 proof -
-fix u
+have "Pi 0 = (2::nat)" by(simp add: Pi.simps)
-show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)"
+show "coprime (Pi (Suc i) ^ u) ((Suc (Suc 0)) ^ length nl)" for u
-proof(rule_tac coprime_exp2_nat)
+using Pi_coprime Pi.simps(1) by force
-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
 qed
 lemma godel_code_get_nth:
 "i < length nl \<Longrightarrow>
 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)
 lemma dvd_power_le: "\<lbrakk>a > Suc 0; a ^ y dvd a ^ l\<rbrakk> \<Longrightarrow> y \<le> l"
 apply(case_tac "y \<le> l", simp, simp)
 apply(subgoal_tac "\<exists> d. y = l + d", auto simp: power_add)
 apply(rule_tac x = "y - l" in exI, simp)
 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:
 "\<lbrakk>(a::nat) > Suc 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> finite {u. a^u dvd y}"
 apply(auto simp: dvd_def)
 fix y
 assume h: "y \<in> ?setx"
 have "Pi m ^ y dvd Pi m ^ l"
 proof -
 have "Pi m ^ y dvd Pi m ^ l * Pi n ^ st"
-using h g
+using h g Pi_power_coprime
-apply(rule_tac n = "Pi k^r" in coprime_dvd_mult_nat)
+by (simp add: coprime_dvd_mult_left_iff)
-apply(rule Pi_power_coprime, simp, simp)
+thus "Pi m^y dvd Pi m^l" using g Pi_power_coprime coprime_dvd_mult_left_iff by blast
-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
 qed
 thus "y \<le> (l::nat)"
 apply(rule_tac a = "Pi m" in power_le_imp_le_exp)
 apply(simp_all add: Pi_gr_1)
 apply(rule_tac dvd_power_le, auto)
 "\<lbrakk>m \<noteq> n; m \<noteq> k; n \<noteq> k;
 \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0"
 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")
 apply(auto)
 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
 = Pi (Suc 0)^st * Pi 0 ^ l *  Pi (Suc (Suc 0)) ^ r")
 apply(simp (no_asm_simp) add: conf_decode1, simp)
 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st *
 Pi (Suc (Suc 0)) ^ r", auto)
 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
 = Pi (Suc (Suc 0))^r * Pi 0 ^ l *  Pi (Suc 0) ^ st")
 apply(simp (no_asm_simp) add: conf_decode1, simp)
 (4 * (st - Suc 0) + 2 * (r mod 2))
 = action_map nact"
 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
 lemma modify_tprog_fetch_state:
 = ns"
 by simp
 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"
 proof(induct xs arbitrary: n)
 case Nil thus "?case"
 qed
 qed
 qed
-lemma [simp]: "2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
+lemma bl2wc_simps[simp]:
-apply(case_tac c, simp, case_tac a)
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
-done
-lemma [simp]:
 "bl2wc (Oc # tl c) = Suc (bl2wc c) - bl2wc c mod 2 "
-apply(case_tac c, case_tac [2] a, simp)
+"bl2wc (Bk # c) = 2*bl2wc (c)"
-apply(auto simp: bl2wc.simps bl2nat.simps bl2nat_double)
+"2 * bl2wc (tl c) = bl2wc c - bl2wc c mod 2 "
-done
+"bl2wc [Oc] = Suc 0"
+"c \<noteq> [] \<Longrightarrow> bl2wc (tl c) = bl2wc c div 2"
-lemma [simp]: "bl2wc (Bk # c) = 2*bl2wc (c)"
+"c \<noteq> [] \<Longrightarrow> bl2wc [hd c] = bl2wc c mod 2"
-apply(simp add: bl2wc.simps bl2nat.simps bl2nat_double)
+"c \<noteq> [] \<Longrightarrow> bl2wc (hd c # d) = 2 * bl2wc d + bl2wc c mod 2"
-done
+"2 * (bl2wc c div 2) = bl2wc c - bl2wc c mod 2"
+"bl2wc (Oc # list) mod 2 = Suc 0"
-lemma [simp]: "bl2wc [Oc] = Suc 0"
+by(cases c;cases "hd c";force simp: bl2wc.simps bl2nat.simps bl2nat_double)+
-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)
 declare code.simps[simp del]
 declare nth_of.simps[simp del]
 text {*
 apply(auto simp: trpl_code.simps
 newleft.simps newrght.simps split: action.splits)
 done
 qed
-lemma [simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
+lemma bl2nat_simps[simp]: "bl2nat (Oc # Oc\<up>x) 0 = (2 * 2 ^ x - Suc 0)"
-apply(induct x)
+"bl2nat (Bk\<up>x) n = 0"
-apply(simp add: bl2nat.simps)
+by(induct x;force simp: bl2nat.simps bl2nat_double exp_ind)+
-apply(simp add: bl2nat.simps bl2nat_double exp_ind)
-done
+lemma bl2nat_exp_zero[simp]: "bl2nat (Oc\<up>y) 0 = 2^y - Suc 0"
-lemma [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)
 by auto
 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
+apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def)
-tape_of_nat_list.simps)
+apply(simp add: tape_of_nl_cons tape_of_nat_def)
-apply(simp add: tape_of_nl_cons tape_of_nat_abv)
 done
 lemma listsum2_append:
 "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n"
 apply(induct n)
 apply(rule_tac ind, simp)
 done
 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
+apply(simp add: tape_of_list_def listsum2.simps
-tape_of_nat_list.simps tape_of_nat_abv)
+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)
 done
 next
 listsum2 (map Suc ys) (length ys) + length ys - 1"
 using length_listsum2_eq[of ys "length ys"]
 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
 inpt.simps trpl_code.simps bl2wc.simps)
 done
 by(simp add: newconf_lemma)
 qed
 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
 lemma lg_power: "x > Suc 0 \<Longrightarrow> lg (x ^ rs) x = rs"
 apply(case_tac rs, simp, simp add: bl2nat.simps)
 done
 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]
 lemma halt_least_step:
 apply(auto simp: nonstop.simps NSTD.simps split: if_splits)
 using conf_trpl_ex[of m lm stpa]
 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}"
 apply(rule_tac finite_power_dvd, auto)
 done
 done
 next
 show "r \<in> {u. x ^ u dvd x ^ r}" by simp
 qed
-lemma lo_power: "x > Suc 0 \<Longrightarrow> lo (x ^ r) x = r"
+lemma lo_power:
-apply(auto simp: lo.simps loR.simps mod_dvd_simp)
+assumes "x > Suc 0" shows "lo (x ^ r) x = r"
-apply(case_tac "x^r", simp_all)
+proof -
-done
+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)
 done

changeset 288	a9003e6d0463
parent 250	745547bdc1c7
child 289	4e50ff177348