--- 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)