1.1 --- a/src/HOL/Fact.thy Wed Jul 15 15:09:33 2009 +0200
1.2 +++ b/src/HOL/Fact.thy Wed Jul 15 15:09:56 2009 +0200
1.3 @@ -2,25 +2,266 @@
1.4 Author : Jacques D. Fleuriot
1.5 Copyright : 1998 University of Cambridge
1.6 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.7 + The integer version of factorial and other additions by Jeremy Avigad.
1.8 *)
1.9
1.10 header{*Factorial Function*}
1.11
1.12 theory Fact
1.13 -imports Main
1.14 +imports NatTransfer
1.15 begin
1.16
1.17 -consts fact :: "nat => nat"
1.18 -primrec
1.19 - fact_0: "fact 0 = 1"
1.20 - fact_Suc: "fact (Suc n) = (Suc n) * fact n"
1.21 +class fact =
1.22
1.23 +fixes
1.24 + fact :: "'a \<Rightarrow> 'a"
1.25
1.26 -lemma fact_gt_zero [simp]: "0 < fact n"
1.27 -by (induct n) auto
1.28 +instantiation nat :: fact
1.29
1.30 -lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
1.31 -by simp
1.32 +begin
1.33 +
1.34 +fun
1.35 + fact_nat :: "nat \<Rightarrow> nat"
1.36 +where
1.37 + fact_0_nat: "fact_nat 0 = Suc 0"
1.38 +| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
1.39 +
1.40 +instance proof qed
1.41 +
1.42 +end
1.43 +
1.44 +(* definitions for the integers *)
1.45 +
1.46 +instantiation int :: fact
1.47 +
1.48 +begin
1.49 +
1.50 +definition
1.51 + fact_int :: "int \<Rightarrow> int"
1.52 +where
1.53 + "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
1.54 +
1.55 +instance proof qed
1.56 +
1.57 +end
1.58 +
1.59 +
1.60 +subsection {* Set up Transfer *}
1.61 +
1.62 +lemma transfer_nat_int_factorial:
1.63 + "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
1.64 + unfolding fact_int_def
1.65 + by auto
1.66 +
1.67 +
1.68 +lemma transfer_nat_int_factorial_closure:
1.69 + "x >= (0::int) \<Longrightarrow> fact x >= 0"
1.70 + by (auto simp add: fact_int_def)
1.71 +
1.72 +declare TransferMorphism_nat_int[transfer add return:
1.73 + transfer_nat_int_factorial transfer_nat_int_factorial_closure]
1.74 +
1.75 +lemma transfer_int_nat_factorial:
1.76 + "fact (int x) = int (fact x)"
1.77 + unfolding fact_int_def by auto
1.78 +
1.79 +lemma transfer_int_nat_factorial_closure:
1.80 + "is_nat x \<Longrightarrow> fact x >= 0"
1.81 + by (auto simp add: fact_int_def)
1.82 +
1.83 +declare TransferMorphism_int_nat[transfer add return:
1.84 + transfer_int_nat_factorial transfer_int_nat_factorial_closure]
1.85 +
1.86 +
1.87 +subsection {* Factorial *}
1.88 +
1.89 +lemma fact_0_int [simp]: "fact (0::int) = 1"
1.90 + by (simp add: fact_int_def)
1.91 +
1.92 +lemma fact_1_nat [simp]: "fact (1::nat) = 1"
1.93 + by simp
1.94 +
1.95 +lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
1.96 + by simp
1.97 +
1.98 +lemma fact_1_int [simp]: "fact (1::int) = 1"
1.99 + by (simp add: fact_int_def)
1.100 +
1.101 +lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
1.102 + by simp
1.103 +
1.104 +lemma fact_plus_one_int:
1.105 + assumes "n >= 0"
1.106 + shows "fact ((n::int) + 1) = (n + 1) * fact n"
1.107 +
1.108 + using prems unfolding fact_int_def
1.109 + by (simp add: nat_add_distrib algebra_simps int_mult)
1.110 +
1.111 +lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.112 + apply (subgoal_tac "n = Suc (n - 1)")
1.113 + apply (erule ssubst)
1.114 + apply (subst fact_Suc_nat)
1.115 + apply simp_all
1.116 +done
1.117 +
1.118 +lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.119 + apply (subgoal_tac "n = (n - 1) + 1")
1.120 + apply (erule ssubst)
1.121 + apply (subst fact_plus_one_int)
1.122 + apply simp_all
1.123 +done
1.124 +
1.125 +lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
1.126 + apply (induct n)
1.127 + apply (auto simp add: fact_plus_one_nat)
1.128 +done
1.129 +
1.130 +lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
1.131 + by (simp add: fact_int_def)
1.132 +
1.133 +lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
1.134 + by (insert fact_nonzero_nat [of n], arith)
1.135 +
1.136 +lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
1.137 + by (auto simp add: fact_int_def)
1.138 +
1.139 +lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
1.140 + by (insert fact_nonzero_nat [of n], arith)
1.141 +
1.142 +lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
1.143 + by (insert fact_nonzero_nat [of n], arith)
1.144 +
1.145 +lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
1.146 + apply (auto simp add: fact_int_def)
1.147 + apply (subgoal_tac "1 = int 1")
1.148 + apply (erule ssubst)
1.149 + apply (subst zle_int)
1.150 + apply auto
1.151 +done
1.152 +
1.153 +lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.154 + apply (induct n)
1.155 + apply force
1.156 + apply (auto simp only: fact_Suc_nat)
1.157 + apply (subgoal_tac "m = Suc n")
1.158 + apply (erule ssubst)
1.159 + apply (rule dvd_triv_left)
1.160 + apply auto
1.161 +done
1.162 +
1.163 +lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
1.164 + apply (case_tac "1 <= n")
1.165 + apply (induct n rule: int_ge_induct)
1.166 + apply (auto simp add: fact_plus_one_int)
1.167 + apply (subgoal_tac "m = i + 1")
1.168 + apply auto
1.169 +done
1.170 +
1.171 +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
1.172 + {i..j+1} = {i..j} Un {j+1}"
1.173 + by auto
1.174 +
1.175 +lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
1.176 + by auto
1.177 +
1.178 +lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
1.179 + by auto
1.180 +
1.181 +lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
1.182 + apply (induct n)
1.183 + apply force
1.184 + apply (subst fact_Suc_nat)
1.185 + apply (subst interval_Suc)
1.186 + apply auto
1.187 +done
1.188 +
1.189 +lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
1.190 + apply (induct n rule: int_ge_induct)
1.191 + apply force
1.192 + apply (subst fact_plus_one_int, assumption)
1.193 + apply (subst interval_plus_one_int)
1.194 + apply auto
1.195 +done
1.196 +
1.197 +lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
1.198 +apply (drule le_imp_less_or_eq)
1.199 +apply (auto dest!: less_imp_Suc_add)
1.200 +apply (induct_tac k, auto)
1.201 +done
1.202 +
1.203 +lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
1.204 + unfolding fact_int_def by auto
1.205 +
1.206 +lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
1.207 + apply (case_tac "m >= 0")
1.208 + apply auto
1.209 + apply (frule fact_gt_zero_int)
1.210 + apply arith
1.211 +done
1.212 +
1.213 +lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
1.214 + fact (m + k) >= fact m"
1.215 + apply (case_tac "m < 0")
1.216 + apply auto
1.217 + apply (induct k rule: int_ge_induct)
1.218 + apply auto
1.219 + apply (subst add_assoc [symmetric])
1.220 + apply (subst fact_plus_one_int)
1.221 + apply auto
1.222 + apply (erule order_trans)
1.223 + apply (subst mult_le_cancel_right1)
1.224 + apply (subgoal_tac "fact (m + i) >= 0")
1.225 + apply arith
1.226 + apply auto
1.227 +done
1.228 +
1.229 +lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
1.230 + apply (insert fact_mono_int_aux [of "n - m" "m"])
1.231 + apply auto
1.232 +done
1.233 +
1.234 +text{*Note that @{term "fact 0 = fact 1"}*}
1.235 +lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
1.236 +apply (drule_tac m = m in less_imp_Suc_add, auto)
1.237 +apply (induct_tac k, auto)
1.238 +done
1.239 +
1.240 +lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
1.241 + fact m < fact ((m + 1) + k)"
1.242 + apply (induct k rule: int_ge_induct)
1.243 + apply (simp add: fact_plus_one_int)
1.244 + apply (subst mult_less_cancel_right1)
1.245 + apply (insert fact_gt_zero_int [of m], arith)
1.246 + apply (subst (2) fact_reduce_int)
1.247 + apply (auto simp add: add_ac)
1.248 + apply (erule order_less_le_trans)
1.249 + apply (subst mult_le_cancel_right1)
1.250 + apply auto
1.251 + apply (subgoal_tac "fact (i + (1 + m)) >= 0")
1.252 + apply force
1.253 + apply (rule fact_ge_zero_int)
1.254 +done
1.255 +
1.256 +lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
1.257 + apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
1.258 + apply auto
1.259 +done
1.260 +
1.261 +lemma fact_num_eq_if_nat: "fact (m::nat) =
1.262 + (if m=0 then 1 else m * fact (m - 1))"
1.263 +by (cases m) auto
1.264 +
1.265 +lemma fact_add_num_eq_if_nat:
1.266 + "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
1.267 +by (cases "m + n") auto
1.268 +
1.269 +lemma fact_add_num_eq_if2_nat:
1.270 + "fact ((m::nat) + n) =
1.271 + (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
1.272 +by (cases m) auto
1.273 +
1.274 +
1.275 +subsection {* @{term fact} and @{term of_nat} *}
1.276
1.277 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
1.278 by auto
1.279 @@ -33,46 +274,10 @@
1.280 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
1.281 by simp
1.282
1.283 -lemma fact_ge_one [simp]: "1 \<le> fact n"
1.284 -by (induct n) auto
1.285 -
1.286 -lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
1.287 -apply (drule le_imp_less_or_eq)
1.288 -apply (auto dest!: less_imp_Suc_add)
1.289 -apply (induct_tac k, auto)
1.290 -done
1.291 -
1.292 -text{*Note that @{term "fact 0 = fact 1"}*}
1.293 -lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
1.294 -apply (drule_tac m = m in less_imp_Suc_add, auto)
1.295 -apply (induct_tac k, auto)
1.296 -done
1.297 -
1.298 lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
1.299 by (auto simp add: positive_imp_inverse_positive)
1.300
1.301 lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
1.302 by (auto intro: order_less_imp_le)
1.303
1.304 -lemma fact_diff_Suc [rule_format]:
1.305 - "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
1.306 -apply (induct n arbitrary: m)
1.307 -apply auto
1.308 -apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
1.309 -done
1.310 -
1.311 -lemma fact_num0: "fact 0 = 1"
1.312 -by auto
1.313 -
1.314 -lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
1.315 -by (cases m) auto
1.316 -
1.317 -lemma fact_add_num_eq_if:
1.318 - "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
1.319 -by (cases "m + n") auto
1.320 -
1.321 -lemma fact_add_num_eq_if2:
1.322 - "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
1.323 -by (cases m) auto
1.324 -
1.325 end
2.1 --- a/src/HOL/GCD.thy Wed Jul 15 15:09:33 2009 +0200
2.2 +++ b/src/HOL/GCD.thy Wed Jul 15 15:09:56 2009 +0200
2.3 @@ -20,6 +20,9 @@
2.4 the congruence relations on the integers. The notion was extended to
2.5 the natural numbers by Chiaeb.
2.6
2.7 +Jeremy Avigad combined all of these, made everything uniform for the
2.8 +natural numbers and the integers, and added a number of new theorems.
2.9 +
2.10 Tobias Nipkow cleaned up a lot.
2.11 *)
2.12
2.13 @@ -27,7 +30,7 @@
2.14 header {* GCD *}
2.15
2.16 theory GCD
2.17 -imports NatTransfer
2.18 +imports Fact
2.19 begin
2.20
2.21 declare One_nat_def [simp del]
2.22 @@ -1751,4 +1754,42 @@
2.23 ultimately show ?thesis by blast
2.24 qed
2.25
2.26 +subsection {* Infinitely many primes *}
2.27 +
2.28 +lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
2.29 +proof-
2.30 + have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
2.31 + from prime_factor_nat [OF f1]
2.32 + obtain p where "prime p" and "p dvd fact n + 1" by auto
2.33 + hence "p \<le> fact n + 1"
2.34 + by (intro dvd_imp_le, auto)
2.35 + {assume "p \<le> n"
2.36 + from `prime p` have "p \<ge> 1"
2.37 + by (cases p, simp_all)
2.38 + with `p <= n` have "p dvd fact n"
2.39 + by (intro dvd_fact_nat)
2.40 + with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
2.41 + by (rule dvd_diff_nat)
2.42 + hence "p dvd 1" by simp
2.43 + hence "p <= 1" by auto
2.44 + moreover from `prime p` have "p > 1" by auto
2.45 + ultimately have False by auto}
2.46 + hence "n < p" by arith
2.47 + with `prime p` and `p <= fact n + 1` show ?thesis by auto
2.48 +qed
2.49 +
2.50 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
2.51 +using next_prime_bound by auto
2.52 +
2.53 +lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
2.54 +proof
2.55 + assume "finite {(p::nat). prime p}"
2.56 + with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
2.57 + by auto
2.58 + then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
2.59 + by auto
2.60 + with bigger_prime [of b] show False by auto
2.61 +qed
2.62 +
2.63 +
2.64 end
3.1 --- a/src/HOL/Library/Binomial.thy Wed Jul 15 15:09:33 2009 +0200
3.2 +++ b/src/HOL/Library/Binomial.thy Wed Jul 15 15:09:56 2009 +0200
3.3 @@ -243,14 +243,8 @@
3.4 ultimately show ?thesis by blast
3.5 qed
3.6
3.7 -lemma fact_setprod: "fact n = setprod id {1 .. n}"
3.8 - apply (induct n, simp)
3.9 - apply (simp only: fact_Suc atLeastAtMostSuc_conv)
3.10 - apply (subst setprod_insert)
3.11 - by simp_all
3.12 -
3.13 lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
3.14 - unfolding fact_setprod
3.15 + unfolding fact_altdef_nat
3.16
3.17 apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
3.18 apply (rule setprod_reindex_cong[where f=Suc])
3.19 @@ -347,7 +341,7 @@
3.20 assumes kn: "k \<le> n"
3.21 shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
3.22 using binomial_fact_lemma[OF kn]
3.23 - by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
3.24 + by (simp add: field_simps of_nat_mult[symmetric])
3.25
3.26 lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
3.27 proof-
3.28 @@ -377,7 +371,7 @@
3.29 have ?thesis using kn
3.30 apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
3.31 gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
3.32 - apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
3.33 + apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
3.34 unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
3.35 unfolding mult_assoc[symmetric]
3.36 unfolding setprod_timesf[symmetric]
3.37 @@ -404,7 +398,7 @@
3.38 proof-
3.39 have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
3.40 unfolding gbinomial_pochhammer
3.41 - pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
3.42 + pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc
3.43 by (simp add: field_simps del: of_nat_Suc)
3.44 also have "\<dots> = ?l" unfolding gbinomial_pochhammer
3.45 by (simp add: ring_simps)
3.46 @@ -420,7 +414,7 @@
3.47 lemma gbinomial_mult_fact:
3.48 "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
3.49 unfolding gbinomial_Suc
3.50 - by (simp_all add: field_simps del: fact_Suc)
3.51 + by (simp_all add: field_simps del: fact_Suc_nat)
3.52
3.53 lemma gbinomial_mult_fact':
3.54 "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
3.55 @@ -438,9 +432,9 @@
3.56
3.57 have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
3.58 unfolding h
3.59 - apply (simp add: ring_simps del: fact_Suc)
3.60 + apply (simp add: ring_simps del: fact_Suc_nat)
3.61 unfolding gbinomial_mult_fact'
3.62 - apply (subst fact_Suc)
3.63 + apply (subst fact_Suc_nat)
3.64 unfolding of_nat_mult
3.65 apply (subst mult_commute)
3.66 unfolding mult_assoc
3.67 @@ -455,7 +449,7 @@
3.68 by simp
3.69 also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
3.70 unfolding gbinomial_mult_fact ..
3.71 - finally have ?thesis by (simp del: fact_Suc) }
3.72 + finally have ?thesis by (simp del: fact_Suc_nat) }
3.73 ultimately show ?thesis by (cases k, auto)
3.74 qed
3.75
4.1 --- a/src/HOL/Library/Formal_Power_Series.thy Wed Jul 15 15:09:33 2009 +0200
4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jul 15 15:09:56 2009 +0200
4.3 @@ -2514,7 +2514,7 @@
4.4 proof-
4.5 {fix n
4.6 have "?l$n = ?r $ n"
4.7 - apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
4.8 + apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
4.9 by (simp add: of_nat_mult ring_simps)}
4.10 then show ?thesis by (simp add: fps_eq_iff)
4.11 qed
4.12 @@ -2530,8 +2530,8 @@
4.13 apply (induct n)
4.14 apply simp
4.15 unfolding th
4.16 - using fact_gt_zero
4.17 - apply (simp add: field_simps del: of_nat_Suc fact.simps)
4.18 + using fact_gt_zero_nat
4.19 + apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
4.20 apply (drule sym)
4.21 by (simp add: ring_simps of_nat_mult power_Suc)}
4.22 note th' = this
4.23 @@ -2697,7 +2697,7 @@
4.24 also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
4.25 using en by (simp add: fps_sin_def)
4.26 also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
4.27 - unfolding fact_Suc of_nat_mult
4.28 + unfolding fact_Suc_nat of_nat_mult
4.29 by (simp add: field_simps del: of_nat_add of_nat_Suc)
4.30 also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
4.31 by (simp add: field_simps del: of_nat_add of_nat_Suc)
4.32 @@ -2721,7 +2721,7 @@
4.33 also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
4.34 using en by (simp add: fps_cos_def)
4.35 also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
4.36 - unfolding fact_Suc of_nat_mult
4.37 + unfolding fact_Suc_nat of_nat_mult
4.38 by (simp add: field_simps del: of_nat_add of_nat_Suc)
4.39 also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
4.40 by (simp add: field_simps del: of_nat_add of_nat_Suc)
4.41 @@ -2747,9 +2747,6 @@
4.42 finally show ?thesis .
4.43 qed
4.44
4.45 -lemma fact_1 [simp]: "fact 1 = 1"
4.46 -unfolding One_nat_def fact_Suc by simp
4.47 -
4.48 lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
4.49 by auto
4.50
4.51 @@ -2766,7 +2763,7 @@
4.52 "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
4.53 unfolding fps_sin_def
4.54 apply (cases n, simp)
4.55 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
4.56 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
4.57 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
4.58 done
4.59
4.60 @@ -2779,7 +2776,7 @@
4.61 lemma fps_cos_nth_add_2:
4.62 "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
4.63 unfolding fps_cos_def
4.64 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
4.65 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
4.66 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
4.67 done
4.68
5.1 --- a/src/HOL/Ln.thy Wed Jul 15 15:09:33 2009 +0200
5.2 +++ b/src/HOL/Ln.thy Wed Jul 15 15:09:56 2009 +0200
5.3 @@ -31,13 +31,13 @@
5.4 qed
5.5
5.6 lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
5.7 - shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
5.8 + shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
5.9 proof (induct n)
5.10 - show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <=
5.11 + show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <=
5.12 x ^ 2 / 2 * (1 / 2) ^ 0"
5.13 by (simp add: real_of_nat_Suc power2_eq_square)
5.14 next
5.15 - fix n
5.16 + fix n :: nat
5.17 assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
5.18 <= x ^ 2 / 2 * (1 / 2) ^ n"
5.19 show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
6.1 --- a/src/HOL/MacLaurin.thy Wed Jul 15 15:09:33 2009 +0200
6.2 +++ b/src/HOL/MacLaurin.thy Wed Jul 15 15:09:56 2009 +0200
6.3 @@ -27,6 +27,10 @@
6.4 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
6.5 by arith
6.6
6.7 +lemma fact_diff_Suc [rule_format]:
6.8 + "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
6.9 + by (subst fact_reduce_nat, auto)
6.10 +
6.11 lemma Maclaurin_lemma2:
6.12 assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
6.13 assumes n: "n = Suc k"
6.14 @@ -47,22 +51,24 @@
6.15 apply (rule_tac [2] DERIV_quotient)
6.16 apply (rule_tac [3] DERIV_const)
6.17 apply (rule_tac [2] DERIV_pow)
6.18 - prefer 3 apply (simp add: fact_diff_Suc)
6.19 + prefer 3
6.20 +
6.21 +apply (simp add: fact_diff_Suc)
6.22 prefer 2 apply simp
6.23 apply (frule less_iff_Suc_add [THEN iffD1], clarify)
6.24 apply (simp del: setsum_op_ivl_Suc)
6.25 apply (insert sumr_offset4 [of "Suc 0"])
6.26 - apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
6.27 + apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
6.28 apply (rule lemma_DERIV_subst)
6.29 apply (rule DERIV_add)
6.30 apply (rule_tac [2] DERIV_const)
6.31 apply (rule DERIV_sumr, clarify)
6.32 prefer 2 apply simp
6.33 - apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
6.34 + apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
6.35 apply (rule DERIV_cmult)
6.36 apply (rule lemma_DERIV_subst)
6.37 apply (best intro!: DERIV_intros)
6.38 - apply (subst fact_Suc)
6.39 + apply (subst fact_Suc_nat)
6.40 apply (subst real_of_nat_mult)
6.41 apply (simp add: mult_ac)
6.42 done
6.43 @@ -114,7 +120,7 @@
6.44 apply (frule less_iff_Suc_add [THEN iffD1], clarify)
6.45 apply (simp del: setsum_op_ivl_Suc)
6.46 apply (insert sumr_offset4 [of "Suc 0"])
6.47 - apply (simp del: setsum_op_ivl_Suc fact_Suc)
6.48 + apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
6.49 done
6.50
6.51 have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
6.52 @@ -174,7 +180,7 @@
6.53 (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
6.54 diff n t / real (fact n) * h ^ n"
6.55 using `difg (Suc m) t = 0`
6.56 - by (simp add: m f_h difg_def del: fact_Suc)
6.57 + by (simp add: m f_h difg_def del: fact_Suc_nat)
6.58 qed
6.59
6.60 qed
7.1 --- a/src/HOL/NewNumberTheory/Binomial.thy Wed Jul 15 15:09:33 2009 +0200
7.2 +++ b/src/HOL/NewNumberTheory/Binomial.thy Wed Jul 15 15:09:56 2009 +0200
7.3 @@ -2,7 +2,7 @@
7.4 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
7.5
7.6
7.7 -Defines factorial and the "choose" function, and establishes basic properties.
7.8 +Defines the "choose" function, and establishes basic properties.
7.9
7.10 The original theory "Binomial" was by Lawrence C. Paulson, based on
7.11 the work of Andy Gordon and Florian Kammueller. The approach here,
7.12 @@ -16,7 +16,7 @@
7.13 header {* Binomial *}
7.14
7.15 theory Binomial
7.16 -imports Cong
7.17 +imports Cong Fact
7.18 begin
7.19
7.20
7.21 @@ -25,7 +25,6 @@
7.22 class binomial =
7.23
7.24 fixes
7.25 - fact :: "'a \<Rightarrow> 'a" and
7.26 binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
7.27
7.28 (* definitions for the natural numbers *)
7.29 @@ -35,13 +34,6 @@
7.30 begin
7.31
7.32 fun
7.33 - fact_nat :: "nat \<Rightarrow> nat"
7.34 -where
7.35 - "fact_nat x =
7.36 - (if x = 0 then 1 else
7.37 - x * fact(x - 1))"
7.38 -
7.39 -fun
7.40 binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
7.41 where
7.42 "binomial_nat n k =
7.43 @@ -60,11 +52,6 @@
7.44 begin
7.45
7.46 definition
7.47 - fact_int :: "int \<Rightarrow> int"
7.48 -where
7.49 - "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
7.50 -
7.51 -definition
7.52 binomial_int :: "int => int \<Rightarrow> int"
7.53 where
7.54 "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
7.55 @@ -76,182 +63,29 @@
7.56
7.57 subsection {* Set up Transfer *}
7.58
7.59 -
7.60 lemma transfer_nat_int_binomial:
7.61 - "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
7.62 "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) =
7.63 nat (binomial n k)"
7.64 - unfolding fact_int_def binomial_int_def
7.65 + unfolding binomial_int_def
7.66 by auto
7.67
7.68 -
7.69 -lemma transfer_nat_int_binomial_closures:
7.70 - "x >= (0::int) \<Longrightarrow> fact x >= 0"
7.71 +lemma transfer_nat_int_binomial_closure:
7.72 "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
7.73 - by (auto simp add: fact_int_def binomial_int_def)
7.74 + by (auto simp add: binomial_int_def)
7.75
7.76 declare TransferMorphism_nat_int[transfer add return:
7.77 - transfer_nat_int_binomial transfer_nat_int_binomial_closures]
7.78 + transfer_nat_int_binomial transfer_nat_int_binomial_closure]
7.79
7.80 lemma transfer_int_nat_binomial:
7.81 - "fact (int x) = int (fact x)"
7.82 "binomial (int n) (int k) = int (binomial n k)"
7.83 unfolding fact_int_def binomial_int_def by auto
7.84
7.85 -lemma transfer_int_nat_binomial_closures:
7.86 - "is_nat x \<Longrightarrow> fact x >= 0"
7.87 +lemma transfer_int_nat_binomial_closure:
7.88 "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
7.89 - by (auto simp add: fact_int_def binomial_int_def)
7.90 + by (auto simp add: binomial_int_def)
7.91
7.92 declare TransferMorphism_int_nat[transfer add return:
7.93 - transfer_int_nat_binomial transfer_int_nat_binomial_closures]
7.94 -
7.95 -
7.96 -subsection {* Factorial *}
7.97 -
7.98 -lemma fact_zero_nat [simp]: "fact (0::nat) = 1"
7.99 - by simp
7.100 -
7.101 -lemma fact_zero_int [simp]: "fact (0::int) = 1"
7.102 - by (simp add: fact_int_def)
7.103 -
7.104 -lemma fact_one_nat [simp]: "fact (1::nat) = 1"
7.105 - by simp
7.106 -
7.107 -lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
7.108 - by (simp add: One_nat_def)
7.109 -
7.110 -lemma fact_one_int [simp]: "fact (1::int) = 1"
7.111 - by (simp add: fact_int_def)
7.112 -
7.113 -lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
7.114 - by simp
7.115 -
7.116 -lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n"
7.117 - by (simp add: One_nat_def)
7.118 -
7.119 -lemma fact_plus_one_int:
7.120 - assumes "n >= 0"
7.121 - shows "fact ((n::int) + 1) = (n + 1) * fact n"
7.122 -
7.123 - using prems by (rule fact_plus_one_nat [transferred])
7.124 -
7.125 -lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
7.126 - by simp
7.127 -
7.128 -lemma fact_reduce_int:
7.129 - assumes "(n::int) > 0"
7.130 - shows "fact n = n * fact (n - 1)"
7.131 -
7.132 - using prems apply (subst tsub_eq [symmetric], auto)
7.133 - apply (rule fact_reduce_nat [transferred])
7.134 - using prems apply auto
7.135 -done
7.136 -
7.137 -declare fact_nat.simps [simp del]
7.138 -
7.139 -lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
7.140 - apply (induct n rule: induct'_nat)
7.141 - apply (auto simp add: fact_plus_one_nat)
7.142 -done
7.143 -
7.144 -lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
7.145 - by (simp add: fact_int_def)
7.146 -
7.147 -lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
7.148 - by (insert fact_nonzero_nat [of n], arith)
7.149 -
7.150 -lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
7.151 - by (auto simp add: fact_int_def)
7.152 -
7.153 -lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
7.154 - by (insert fact_nonzero_nat [of n], arith)
7.155 -
7.156 -lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
7.157 - by (insert fact_nonzero_nat [of n], arith)
7.158 -
7.159 -lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
7.160 - apply (auto simp add: fact_int_def)
7.161 - apply (subgoal_tac "1 = int 1")
7.162 - apply (erule ssubst)
7.163 - apply (subst zle_int)
7.164 - apply auto
7.165 -done
7.166 -
7.167 -lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
7.168 - apply (induct n rule: induct'_nat)
7.169 - apply (auto simp add: fact_plus_one_nat)
7.170 - apply (subgoal_tac "m = n + 1")
7.171 - apply auto
7.172 -done
7.173 -
7.174 -lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
7.175 - apply (case_tac "1 <= n")
7.176 - apply (induct n rule: int_ge_induct)
7.177 - apply (auto simp add: fact_plus_one_int)
7.178 - apply (subgoal_tac "m = i + 1")
7.179 - apply auto
7.180 -done
7.181 -
7.182 -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
7.183 - {i..j+1} = {i..j} Un {j+1}"
7.184 - by auto
7.185 -
7.186 -lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
7.187 - by auto
7.188 -
7.189 -lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
7.190 - apply (induct n rule: induct'_nat)
7.191 - apply force
7.192 - apply (subst fact_plus_one_nat)
7.193 - apply (subst interval_plus_one_nat)
7.194 - apply auto
7.195 -done
7.196 -
7.197 -lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
7.198 - apply (induct n rule: int_ge_induct)
7.199 - apply force
7.200 - apply (subst fact_plus_one_int, assumption)
7.201 - apply (subst interval_plus_one_int)
7.202 - apply auto
7.203 -done
7.204 -
7.205 -subsection {* Infinitely many primes *}
7.206 -
7.207 -lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
7.208 -proof-
7.209 - have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
7.210 - from prime_factor_nat [OF f1]
7.211 - obtain p where "prime p" and "p dvd fact n + 1" by auto
7.212 - hence "p \<le> fact n + 1"
7.213 - by (intro dvd_imp_le, auto)
7.214 - {assume "p \<le> n"
7.215 - from `prime p` have "p \<ge> 1"
7.216 - by (cases p, simp_all)
7.217 - with `p <= n` have "p dvd fact n"
7.218 - by (intro dvd_fact_nat)
7.219 - with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
7.220 - by (rule dvd_diff_nat)
7.221 - hence "p dvd 1" by simp
7.222 - hence "p <= 1" by auto
7.223 - moreover from `prime p` have "p > 1" by auto
7.224 - ultimately have False by auto}
7.225 - hence "n < p" by arith
7.226 - with `prime p` and `p <= fact n + 1` show ?thesis by auto
7.227 -qed
7.228 -
7.229 -lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
7.230 -using next_prime_bound by auto
7.231 -
7.232 -lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
7.233 -proof
7.234 - assume "finite {(p::nat). prime p}"
7.235 - with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
7.236 - by auto
7.237 - then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
7.238 - by auto
7.239 - with bigger_prime [of b] show False by auto
7.240 -qed
7.241 + transfer_int_nat_binomial transfer_int_nat_binomial_closure]
7.242
7.243
7.244 subsection {* Binomial coefficients *}
8.1 --- a/src/HOL/Transcendental.thy Wed Jul 15 15:09:33 2009 +0200
8.2 +++ b/src/HOL/Transcendental.thy Wed Jul 15 15:09:56 2009 +0200
8.3 @@ -621,19 +621,19 @@
8.4
8.5 subsection{* Some properties of factorials *}
8.6
8.7 -lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
8.8 +lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
8.9 by auto
8.10
8.11 -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
8.12 +lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
8.13 by auto
8.14
8.15 -lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
8.16 +lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
8.17 by simp
8.18
8.19 -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
8.20 +lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
8.21 by (auto simp add: positive_imp_inverse_positive)
8.22
8.23 -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
8.24 +lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
8.25 by (auto intro: order_less_imp_le)
8.26
8.27 subsection {* Derivability of power series *}
8.28 @@ -1604,11 +1604,11 @@
8.29 apply (rotate_tac 2)
8.30 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
8.31 unfolding One_nat_def
8.32 -apply (auto simp del: fact_Suc)
8.33 +apply (auto simp del: fact_Suc_nat)
8.34 apply (frule sums_unique)
8.35 -apply (auto simp del: fact_Suc)
8.36 +apply (auto simp del: fact_Suc_nat)
8.37 apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
8.38 -apply (auto simp del: fact_Suc)
8.39 +apply (auto simp del: fact_Suc_nat)
8.40 apply (erule sums_summable)
8.41 apply (case_tac "m=0")
8.42 apply (simp (no_asm_simp))
8.43 @@ -1617,24 +1617,24 @@
8.44 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
8.45 apply (subgoal_tac "x*x < 2*3", simp)
8.46 apply (rule mult_strict_mono)
8.47 -apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
8.48 -apply (subst fact_Suc)
8.49 -apply (subst fact_Suc)
8.50 -apply (subst fact_Suc)
8.51 -apply (subst fact_Suc)
8.52 +apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
8.53 +apply (subst fact_Suc_nat)
8.54 +apply (subst fact_Suc_nat)
8.55 +apply (subst fact_Suc_nat)
8.56 +apply (subst fact_Suc_nat)
8.57 apply (subst real_of_nat_mult)
8.58 apply (subst real_of_nat_mult)
8.59 apply (subst real_of_nat_mult)
8.60 apply (subst real_of_nat_mult)
8.61 -apply (simp (no_asm) add: divide_inverse del: fact_Suc)
8.62 -apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
8.63 +apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
8.64 +apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
8.65 apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
8.66 -apply (auto simp add: mult_assoc simp del: fact_Suc)
8.67 +apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
8.68 apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
8.69 -apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
8.70 +apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
8.71 apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
8.72 apply (erule ssubst)+
8.73 -apply (auto simp del: fact_Suc)
8.74 +apply (auto simp del: fact_Suc_nat)
8.75 apply (subgoal_tac "0 < x ^ (4 * m) ")
8.76 prefer 2 apply (simp only: zero_less_power)
8.77 apply (simp (no_asm_simp) add: mult_less_cancel_left)
8.78 @@ -1670,24 +1670,24 @@
8.79 apply (rule_tac y =
8.80 "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
8.81 in order_less_trans)
8.82 -apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc)
8.83 +apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
8.84 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
8.85 apply (rule sumr_pos_lt_pair)
8.86 apply (erule sums_summable, safe)
8.87 unfolding One_nat_def
8.88 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
8.89 - del: fact_Suc)
8.90 + del: fact_Suc_nat)
8.91 apply (rule real_mult_inverse_cancel2)
8.92 apply (rule real_of_nat_fact_gt_zero)+
8.93 -apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
8.94 +apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
8.95 apply (subst fact_lemma)
8.96 -apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
8.97 +apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
8.98 apply (simp only: real_of_nat_mult)
8.99 apply (rule mult_strict_mono, force)
8.100 apply (rule_tac [3] real_of_nat_ge_zero)
8.101 prefer 2 apply force
8.102 apply (rule real_of_nat_less_iff [THEN iffD2])
8.103 -apply (rule fact_less_mono, auto)
8.104 +apply (rule fact_less_mono_nat, auto)
8.105 done
8.106
8.107 lemmas cos_two_neq_zero [simp] = cos_two_less_zero [THEN less_imp_neq]