summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Multivariate_Analysis/ex/Approximations.thy

changeset 63417 | c184ec919c70 |

parent 63040 | eb4ddd18d635 |

1.1 --- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Fri Jul 08 23:43:11 2016 +0200 1.2 +++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Sat Jul 09 13:26:16 2016 +0200 1.3 @@ -185,11 +185,11 @@ 1.4 also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)" 1.5 proof (intro setsum.cong refl) 1.6 fix k assume k: "k \<in> {..n}" 1.7 - have "fact n = (\<Prod>i=1..n. real i)" by (rule fact_altdef) 1.8 + have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod) 1.9 also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto 1.10 also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)" 1.11 by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto 1.12 - also have "\<dots> = fact k" by (simp only: fact_altdef) 1.13 + also have "\<dots> = fact k" by (simp add: fact_setprod) 1.14 finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp 1.15 qed 1.16 also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps)