--- a/src/HOL/Arith_Tools.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Arith_Tools.thy Wed Feb 25 07:42:20 2009 +0100
@@ -68,8 +68,9 @@
apply (subst add_eq_if)
apply (simp split add: nat.split
del: nat_numeral_1_eq_1
- add: numeral_1_eq_Suc_0 [symmetric] Let_def
- neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
+ neg_number_of_pred_iff_0)
done
lemma nat_rec_number_of [simp]:
@@ -89,7 +90,8 @@
apply (subst add_eq_if)
apply (simp split add: nat.split
del: nat_numeral_1_eq_1
- add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
+ add: nat_numeral_1_eq_1 [symmetric]
+ numeral_1_eq_Suc_0 [symmetric]
neg_number_of_pred_iff_0)
done
--- a/src/HOL/Divides.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Divides.thy Wed Feb 25 07:42:20 2009 +0100
@@ -194,6 +194,12 @@
apply(fastsimp simp add: mult_assoc)
done
+lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m"
+ apply (subgoal_tac "k dvd (m div n) *n + m mod n")
+ apply (simp add: mod_div_equality)
+ apply (simp only: dvd_add dvd_mult)
+ done
+
text {* Addition respects modular equivalence. *}
lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
@@ -484,9 +490,9 @@
from divmod_rel have divmod_m_n: "divmod_rel m n (m div n) (m mod n)" .
with assms have m_div_n: "m div n \<ge> 1"
by (cases "m div n") (auto simp add: divmod_rel_def)
- from assms divmod_m_n have "divmod_rel (m - n) n (m div n - 1) (m mod n)"
+ from assms divmod_m_n have "divmod_rel (m - n) n (m div n - Suc 0) (m mod n)"
by (cases "m div n") (auto simp add: divmod_rel_def)
- with divmod_eq have "divmod (m - n) n = (m div n - 1, m mod n)" by simp
+ with divmod_eq have "divmod (m - n) n = (m div n - Suc 0, m mod n)" by simp
moreover from divmod_div_mod have "divmod (m - n) n = ((m - n) div n, (m - n) mod n)" .
ultimately have "m div n = Suc ((m - n) div n)"
and "m mod n = (m - n) mod n" using m_div_n by simp_all
@@ -810,6 +816,9 @@
lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
by (simp add: dvd_def)
+lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
+by (simp add: dvd_def)
+
lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
unfolding dvd_def
by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
@@ -848,12 +857,6 @@
apply (blast intro: mod_mult_distrib2 [symmetric])
done
-lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n; k dvd n |] ==> k dvd m"
- apply (subgoal_tac "k dvd (m div n) *n + m mod n")
- apply (simp add: mod_div_equality)
- apply (simp only: dvd_add dvd_mult)
- done
-
lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
by (blast intro: dvd_mod_imp_dvd dvd_mod)
--- a/src/HOL/Fact.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Fact.thy Wed Feb 25 07:42:20 2009 +0100
@@ -58,7 +58,7 @@
"n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
apply (induct n arbitrary: m)
apply auto
-apply (drule_tac x = "m - 1" in meta_spec, auto)
+apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
done
lemma fact_num0: "fact 0 = 1"
--- a/src/HOL/GCD.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/GCD.thy Wed Feb 25 07:42:20 2009 +0100
@@ -60,9 +60,12 @@
lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
by simp
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
by simp
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+ unfolding One_nat_def by (rule gcd_1)
+
declare gcd.simps [simp del]
text {*
@@ -116,9 +119,12 @@
apply (blast intro: dvd_trans)
done
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
by (simp add: gcd_commute)
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+ unfolding One_nat_def by (rule gcd_1_left)
+
text {*
\medskip Multiplication laws
*}
--- a/src/HOL/Groebner_Basis.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Wed Feb 25 07:42:20 2009 +0100
@@ -147,7 +147,7 @@
next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
next show "pwr x 0 = r1" using pwr_0 .
-next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
+next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
--- a/src/HOL/Int.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Int.thy Wed Feb 25 07:42:20 2009 +0100
@@ -832,8 +832,8 @@
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
- thus ?thesis by (simp del: of_nat_Suc of_nat_add
- add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
+ add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
qed
lemma bin_less_0_simps:
@@ -1165,8 +1165,8 @@
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
- thus ?thesis by (simp del: of_nat_Suc of_nat_add
- add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric])
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
+ add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
qed
text {* Less-Than or Equals *}
@@ -1785,11 +1785,12 @@
lemma int_val_lemma:
"(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
+unfolding One_nat_def
apply (induct n, simp)
apply (intro strip)
apply (erule impE, simp)
apply (erule_tac x = n in allE, simp)
-apply (case_tac "k = f (n+1) ")
+apply (case_tac "k = f (Suc n)")
apply force
apply (erule impE)
apply (simp add: abs_if split add: split_if_asm)
@@ -1803,6 +1804,7 @@
f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
in int_val_lemma)
+unfolding One_nat_def
apply simp
apply (erule exE)
apply (rule_tac x = "i+m" in exI, arith)
--- a/src/HOL/IntDiv.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/IntDiv.thy Wed Feb 25 07:42:20 2009 +0100
@@ -1228,7 +1228,7 @@
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
-apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
+apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
apply (erule ssubst)
apply (simp only: power_add)
apply simp_all
--- a/src/HOL/Integration.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Integration.thy Wed Feb 25 07:42:20 2009 +0100
@@ -134,7 +134,7 @@
apply (frule partition [THEN iffD1], safe)
apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
apply (case_tac "psize D = 0")
-apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
+apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
done
lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
@@ -145,7 +145,7 @@
apply (rotate_tac 2)
apply (drule_tac x = "psize D" in spec)
apply (rule ccontr)
-apply (drule_tac n = "psize D - 1" in partition_lt)
+apply (drule_tac n = "psize D - Suc 0" in partition_lt)
apply auto
done
--- a/src/HOL/List.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/List.thy Wed Feb 25 07:42:20 2009 +0100
@@ -1438,10 +1438,10 @@
apply (auto split:nat.split)
done
-lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)"
by(induct xs)(auto simp:neq_Nil_conv)
-lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
+lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs"
by (induct xs, simp, case_tac xs, simp_all)
@@ -1588,7 +1588,7 @@
done
lemma butlast_take:
- "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
+ "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs"
by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
@@ -1639,7 +1639,7 @@
done
lemma take_hd_drop:
- "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
+ "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
apply(induct xs arbitrary: n)
apply simp
apply(simp add:drop_Cons split:nat.split)
@@ -2458,7 +2458,7 @@
done
lemma length_remove1:
- "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
+ "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)"
apply (induct xs)
apply (auto dest!:length_pos_if_in_set)
done
--- a/src/HOL/MacLaurin.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/MacLaurin.thy Wed Feb 25 07:42:20 2009 +0100
@@ -81,7 +81,7 @@
prefer 2 apply simp
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
apply (rule lemma_DERIV_subst)
apply (rule DERIV_add)
@@ -124,7 +124,7 @@
have g2: "g 0 = 0 & g h = 0"
apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
- apply (cut_tac n = m and k = 1 in sumr_offset2)
+ apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
done
@@ -144,7 +144,7 @@
apply (simp add: m difg_def)
apply (frule less_iff_Suc_add [THEN iffD1], clarify)
apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
done
@@ -552,6 +552,10 @@
"[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
by auto
+text {* TODO: move to Parity.thy *}
+lemma nat_odd_1 [simp]: "odd (1::nat)"
+ unfolding even_nat_def by simp
+
lemma Maclaurin_sin_bound:
"abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
--- a/src/HOL/NSA/NSA.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/NSA/NSA.thy Wed Feb 25 07:42:20 2009 +0100
@@ -157,7 +157,7 @@
by transfer (rule norm_divide)
lemma hypreal_hnorm_def [simp]:
- "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
+ "\<And>r::hypreal. hnorm r = \<bar>r\<bar>"
by transfer (rule real_norm_def)
lemma hnorm_add_less:
--- a/src/HOL/Nat.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Nat.thy Wed Feb 25 07:42:20 2009 +0100
@@ -196,8 +196,8 @@
instance proof
fix n m q :: nat
- show "0 \<noteq> (1::nat)" by simp
- show "1 * n = n" by simp
+ show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
+ show "1 * n = n" unfolding One_nat_def by simp
show "n * m = m * n" by (induct n) simp_all
show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
@@ -307,18 +307,24 @@
lemmas nat_distrib =
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
-lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
+lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
apply (induct m)
apply simp
apply (induct n)
apply auto
done
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
+lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastsimp)
done
+lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule mult_eq_1_iff)
+
+lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule one_eq_mult_iff)
+
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
proof -
have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
@@ -465,11 +471,11 @@
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
unfolding less_Suc_eq_le le_less ..
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
- by (simp add: less_Suc_eq)
+lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+ unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
by simp
@@ -800,6 +806,7 @@
done
lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
+ unfolding One_nat_def
apply (cases n)
apply blast
apply (frule (1) ex_least_nat_le)
@@ -1089,7 +1096,7 @@
apply simp_all
done
-lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
+lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
apply (induct m)
apply simp
apply (case_tac n)
@@ -1125,7 +1132,7 @@
by (cases m) (auto intro: le_add1)
text {* Lemma for @{text gcd} *}
-lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
+lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
apply (drule sym)
apply (rule disjCI)
apply (rule nat_less_cases, erule_tac [2] _)
@@ -1164,7 +1171,7 @@
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- by simp
+ unfolding One_nat_def by simp
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1276,7 +1283,7 @@
end
lemma of_nat_id [simp]: "of_nat n = n"
- by (induct n) auto
+ by (induct n) (auto simp add: One_nat_def)
lemma of_nat_eq_id [simp]: "of_nat = id"
by (auto simp add: expand_fun_eq)
@@ -1381,7 +1388,7 @@
apply(induct_tac k)
apply simp
apply(erule_tac x="m+n" in meta_allE)
-apply(erule_tac x="m+n+1" in meta_allE)
+apply(erule_tac x="Suc(m+n)" in meta_allE)
apply simp
done
--- a/src/HOL/NatBin.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/NatBin.thy Wed Feb 25 07:42:20 2009 +0100
@@ -159,6 +159,21 @@
unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_add_distrib)
+lemma nat_number_of_add_1 [simp]:
+ "number_of v + (1::nat) =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_number_of [simp]:
+ "(1::nat) + number_of v =
+ (if v < Int.Pls then 1 else number_of (Int.succ v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by (simp add: nat_add_distrib)
+
+lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)"
+ by (rule int_int_eq [THEN iffD1]) simp
+
subsubsection{*Subtraction *}
@@ -178,6 +193,12 @@
unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
by auto
+lemma nat_number_of_diff_1 [simp]:
+ "number_of v - (1::nat) =
+ (if v \<le> Int.Pls then 0 else number_of (Int.pred v))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
subsubsection{*Multiplication *}
@@ -442,19 +463,13 @@
(* These two can be useful when m = number_of... *)
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
-apply (case_tac "m")
-apply (simp_all add: numerals)
-done
+ unfolding One_nat_def by (cases m) simp_all
subsection{*Comparisons involving (0::nat) *}
--- a/src/HOL/Power.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Power.thy Wed Feb 25 07:42:20 2009 +0100
@@ -31,7 +31,7 @@
by (induct n) (simp_all add: power_Suc)
lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
- by (simp add: power_Suc)
+ unfolding One_nat_def by (simp add: power_Suc)
lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
by (induct n) (simp_all add: power_Suc mult_assoc)
@@ -366,8 +366,8 @@
"of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
by (induct n, simp_all add: power_Suc of_nat_mult)
-lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
-by (insert one_le_power [of i n], simp)
+lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
+by (rule one_le_power [of i n, unfolded One_nat_def])
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct "n", auto)
@@ -452,4 +452,3 @@
*}
end
-
--- a/src/HOL/RealDef.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/RealDef.thy Wed Feb 25 07:42:20 2009 +0100
@@ -705,6 +705,9 @@
lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
by (simp add: real_of_nat_def)
+lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
+by (simp add: real_of_nat_def)
+
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
by (simp add: real_of_nat_def)
--- a/src/HOL/RealPow.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/RealPow.thy Wed Feb 25 07:42:20 2009 +0100
@@ -44,7 +44,8 @@
by (insert power_decreasing [of 1 "Suc n" r], simp)
lemma realpow_minus_mult [rule_format]:
- "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+ "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+unfolding One_nat_def
apply (simp split add: nat_diff_split)
done
--- a/src/HOL/Relation_Power.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Relation_Power.thy Wed Feb 25 07:42:20 2009 +0100
@@ -61,16 +61,16 @@
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
proof -
- have "f((f^n) x) = (f^(n+1)) x" by simp
+ have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
also have "\<dots> = (f^n o f^1) x" by (simp only: funpow_add)
- also have "\<dots> = (f^n)(f x)" by simp
+ also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
finally show ?thesis .
qed
lemma rel_pow_1 [simp]:
fixes R :: "('a*'a)set"
shows "R^1 = R"
- by simp
+ unfolding One_nat_def by simp
lemma rel_pow_0_I: "(x,x) : R^0"
by simp
--- a/src/HOL/SEQ.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/SEQ.thy Wed Feb 25 07:42:20 2009 +0100
@@ -338,10 +338,10 @@
done
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
-by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
+by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
-by (rule_tac k="1" in LIMSEQ_offset, simp)
+by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
--- a/src/HOL/Series.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Series.thy Wed Feb 25 07:42:20 2009 +0100
@@ -312,6 +312,7 @@
shows "\<lbrakk>summable f;
\<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
\<Longrightarrow> setsum f {0..<k} < suminf f"
+unfolding One_nat_def
apply (subst suminf_split_initial_segment [where k="k"])
apply assumption
apply simp
@@ -537,7 +538,7 @@
apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
prefer 2
apply clarify
- apply(erule_tac x = "n - 1" in allE)
+ apply(erule_tac x = "n - Suc 0" in allE)
apply (simp add:diff_Suc split:nat.splits)
apply (blast intro: norm_ratiotest_lemma)
apply (rule_tac x = "Suc N" in exI, clarify)
--- a/src/HOL/SetInterval.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/SetInterval.thy Wed Feb 25 07:42:20 2009 +0100
@@ -352,11 +352,11 @@
corollary image_Suc_atLeastAtMost[simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
-using image_add_atLeastAtMost[where k=1] by simp
+using image_add_atLeastAtMost[where k="Suc 0"] by simp
corollary image_Suc_atLeastLessThan[simp]:
"Suc ` {i..<j} = {Suc i..<Suc j}"
-using image_add_atLeastLessThan[where k=1] by simp
+using image_add_atLeastLessThan[where k="Suc 0"] by simp
lemma image_add_int_atLeastLessThan:
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
@@ -556,7 +556,7 @@
qed
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
-apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - 1"])
+apply (rule card_bij_eq [of "Suc" _ _ "\<lambda>x. x - Suc 0"])
apply simp
apply fastsimp
apply auto
@@ -803,7 +803,7 @@
lemma setsum_head_upt_Suc:
"m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}"
-apply(insert setsum_head_Suc[of m "n - 1" f])
+apply(insert setsum_head_Suc[of m "n - Suc 0" f])
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
done
@@ -835,11 +835,11 @@
corollary setsum_shift_bounds_cl_Suc_ivl:
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
-by (simp add:setsum_shift_bounds_cl_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
corollary setsum_shift_bounds_Suc_ivl:
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
-by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
+by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
lemma setsum_shift_lb_Suc0_0:
"f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}"
@@ -883,6 +883,7 @@
by (rule setsum_addf)
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
+ unfolding One_nat_def
by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac)
also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
by (simp add: left_distrib right_distrib)
@@ -890,7 +891,7 @@
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)
also from ngt1
have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
- by (simp only: mult_ac gauss_sum [of "n - 1"])
+ by (simp only: mult_ac gauss_sum [of "n - 1"], unfold One_nat_def)
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]])
finally show ?thesis by (simp add: algebra_simps)
next
@@ -906,7 +907,8 @@
"((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
of_nat(n) * (a + (a + of_nat(n - 1)*d))"
by (rule arith_series_general)
- thus ?thesis by (auto simp add: of_nat_id)
+ thus ?thesis
+ unfolding One_nat_def by (auto simp add: of_nat_id)
qed
lemma arith_series_int:
--- a/src/HOL/Transcendental.thy Wed Feb 25 07:42:11 2009 +0100
+++ b/src/HOL/Transcendental.thy Wed Feb 25 07:42:20 2009 +0100
@@ -120,7 +120,7 @@
case (Suc n)
have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
(\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
- using Suc.hyps by auto
+ using Suc.hyps unfolding One_nat_def by auto
also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
finally show ?case .
qed auto
@@ -187,16 +187,18 @@
((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
proof -
- have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" by auto
+ have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
have "\<forall> n. ?f n \<le> ?f (Suc n)"
proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
moreover
have "\<forall> n. ?g (Suc n) \<le> ?g n"
- proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] by auto qed
+ proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
+ unfolding One_nat_def by auto qed
moreover
have "\<forall> n. ?f n \<le> ?g n"
- proof fix n show "?f n \<le> ?g n" using fg_diff a_pos by auto qed
+ proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
+ unfolding One_nat_def by auto qed
moreover
have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
proof (rule LIMSEQ_I)
@@ -904,7 +906,7 @@
proof -
have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
by (rule sums_unique [OF series_zero], simp add: power_0_left)
- thus ?thesis by simp
+ thus ?thesis unfolding One_nat_def by simp
qed
lemma exp_zero [simp]: "exp 0 = 1"
@@ -1234,10 +1236,11 @@
show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto
{ fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+ unfolding One_nat_def
by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
}
qed
- hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" by auto
+ hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos .
ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
by (rule DERIV_diff)
@@ -1514,6 +1517,7 @@
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
+unfolding One_nat_def
apply (rule lemma_DERIV_subst)
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
apply (rule DERIV_pow, auto)
@@ -1635,7 +1639,7 @@
sums sin x"
unfolding sin_def
by (rule sin_converges [THEN sums_summable, THEN sums_group], simp)
- thus ?thesis by (simp add: mult_ac)
+ thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
qed
lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
@@ -1647,6 +1651,7 @@
apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp)
apply (rotate_tac 2)
apply (drule sin_paired [THEN sums_unique, THEN ssubst])
+unfolding One_nat_def
apply (auto simp del: fact_Suc realpow_Suc)
apply (frule sums_unique)
apply (auto simp del: fact_Suc realpow_Suc)
@@ -1720,6 +1725,7 @@
apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
+unfolding One_nat_def
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
@@ -2792,7 +2798,7 @@
lemma monoseq_arctan_series: fixes x :: real
assumes "\<bar>x\<bar> \<le> 1" shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
-proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def by auto
+proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def One_nat_def by auto
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2823,7 +2829,7 @@
lemma zeroseq_arctan_series: fixes x :: real
assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
-proof (cases "x = 0") case True thus ?thesis by (auto simp add: LIMSEQ_const)
+proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2831,12 +2837,14 @@
proof (cases "\<bar>x\<bar> < 1")
case True hence "norm x < 1" by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
- show ?thesis unfolding inverse_eq_divide Suc_plus1 using LIMSEQ_linear[OF _ pos2] by auto
+ have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
+ unfolding inverse_eq_divide Suc_plus1 by simp
+ then show ?thesis using pos2 by (rule LIMSEQ_linear)
next
case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
- hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" by auto
+ hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
- show ?thesis unfolding n_eq by auto
+ show ?thesis unfolding n_eq Suc_plus1 by auto
qed
qed
@@ -2989,7 +2997,7 @@
from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
from bounds[of m, unfolded this atLeastAtMost_iff]
have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))" by auto
- also have "\<dots> = ?c x n" by auto
+ also have "\<dots> = ?c x n" unfolding One_nat_def by auto
also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
finally show ?thesis .
next
@@ -2998,7 +3006,7 @@
hence m_plus: "2 * (m + 1) = n + 1" by auto
from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))" by auto
- also have "\<dots> = - ?c x n" by auto
+ also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
finally show ?thesis .
qed
@@ -3011,7 +3019,9 @@
ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
hence "?diff 1 n \<le> ?a 1 n" by auto
}
- have "?a 1 ----> 0" unfolding LIMSEQ_rabs_zero power_one divide_inverse by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+ have "?a 1 ----> 0"
+ unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
+ by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
have "?diff 1 ----> 0"
proof (rule LIMSEQ_I)
fix r :: real assume "0 < r"
@@ -3031,7 +3041,7 @@
have "- (pi / 2) < 0" using pi_gt_zero by auto
have "- (2 * pi) < 0" using pi_gt_zero by auto
- have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" by auto
+ have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
@@ -3179,4 +3189,4 @@
apply (erule polar_ex2)
done
-end
+end