author bulwahn Fri, 02 Mar 2012 09:35:33 +0100 changeset 46757 ad878aff9c15 parent 46756 faf62905cd53 child 46758 4106258260b3
removing finiteness goals
 src/HOL/Library/Binomial.thy file | annotate | diff | comparison | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions src/HOL/SupInf.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/Binomial.thy	Fri Mar 02 09:35:32 2012 +0100
+++ b/src/HOL/Library/Binomial.thy	Fri Mar 02 09:35:33 2012 +0100
@@ -203,16 +203,14 @@

lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
proof-
-  have th: "finite {0..n}" "finite {Suc n}" "{0..n} \<inter> {Suc n} = {}" by auto
have eq: "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
-  show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp
+  show ?thesis unfolding eq by (simp add: field_simps)
qed

lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
proof-
-  have th: "finite {0}" "finite {1..Suc n}" "{0} \<inter> {1.. Suc n} = {}" by auto
have eq: "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
-  show ?thesis unfolding eq setprod_Un_disjoint[OF th] by simp
+  show ?thesis unfolding eq by simp
qed

@@ -221,7 +219,7 @@
{assume "n=0" then have ?thesis by simp}
moreover
{fix m assume m: "n = Suc m"
-    have ?thesis  unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..}
+    have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..}
ultimately show ?thesis by (cases n, auto)
qed
```
```--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 02 09:35:32 2012 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Mar 02 09:35:33 2012 +0100
@@ -420,10 +420,9 @@
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))"
proof-
{assume n: "n \<noteq> 0"
-    have fN: "finite {0 .. n}" by simp
have "(X * f) \$n = (\<Sum>i = 0..n. X \$ i * f \$ (n - i))" by (simp add: fps_mult_nth)
also have "\<dots> = f \$ (n - 1)"
-      using n by (simp add: X_def mult_delta_left setsum_delta [OF fN])
+      using n by (simp add: X_def mult_delta_left setsum_delta)
finally have ?thesis using n by simp }
moreover
{assume n: "n=0" hence ?thesis by (simp add: fps_mult_nth X_def)}
@@ -686,7 +685,6 @@
{fix n::nat assume np: "n >0 "
from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto
have d: "{0} \<inter> {1 .. n} = {}" by auto
-    have f: "finite {0::nat}" "finite {1..n}" by auto
from f0 np have th0: "- (inverse f\$n) =
(setsum (\<lambda>i. f\$i * natfun_inverse f (n - i)) {1..n}) / (f\$0)"
by (cases n, simp, simp add: divide_inverse fps_inverse_def)
@@ -698,8 +696,7 @@
unfolding fps_mult_nth ifn ..
also have "\<dots> = f\$0 * natfun_inverse f n
+ (\<Sum>i = 1..n. f\$i * natfun_inverse f (n-i))"
-      unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]]
-      by simp
also have "\<dots> = 0" unfolding th1 ifn by simp
finally have "(inverse f * f)\$n = 0" unfolding c . }
with th0 show ?thesis by (simp add: fps_eq_iff)
@@ -1449,8 +1446,7 @@
fixes m :: nat and a :: "('a::comm_ring_1) fps"
shows "(a ^ Suc m)\$n = setsum (\<lambda>v. setprod (\<lambda>j. a \$ (v!j)) {0..m}) (natpermute n (m+1))"
proof-
-  have f: "finite {0 ..m}" by simp
-  have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp
+  have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" by (simp add: setprod_constant)
show ?thesis unfolding th0 fps_setprod_nth ..
qed
lemma fps_power_nth:
@@ -1565,7 +1561,6 @@
{assume "k=0" hence ?thesis by simp }
moreover
{fix h assume h: "k = Suc h"
-    have fh: "finite {0..h}" by simp
have eq1: "fps_radical r k a ^ k \$ 0 = (\<Prod>j\<in>{0..h}. fps_radical r k a \$ (replicate k 0) ! j)"
unfolding fps_power_nth h by simp
also have "\<dots> = (\<Prod>j\<in>{0..h}. r k (a\$0))"
@@ -1575,7 +1570,7 @@
apply (subgoal_tac "replicate k (0::nat) ! x = 0")
by (auto intro: nth_replicate simp del: replicate.simps)
also have "\<dots> = a\$0"
-      unfolding setprod_constant[OF fh] using r by (simp add: h)
+      using r by (simp add: h setprod_constant)
finally have ?thesis using h by simp}
ultimately show ?thesis by (cases k, auto)
qed
@@ -1618,7 +1613,6 @@
using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp}
moreover
{fix n1 assume n1: "n = Suc n1"
-          have fK: "finite {0..k}" by simp
have nz: "n \<noteq> 0" using n1 by arith
let ?Pnk = "natpermute n (k + 1)"
let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}"
@@ -1639,7 +1633,7 @@
apply (rule setprod_cong, simp)
using i r0 by (simp del: replicate.simps)
also have "\<dots> = (fps_radical r (Suc k) a \$ n) * r (Suc k) (a\$0) ^ k"
-            unfolding setprod_gen_delta[OF fK] using i r0 by simp
+            using i r0 by (simp add: setprod_gen_delta)
finally show ?ths .
qed
then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r \$ n * r (Suc k) (a \$ 0) ^ k"
@@ -1737,7 +1731,6 @@
moreover
{assume H: "a^Suc k = b"
have ceq: "card {0..k} = Suc k" by simp
-    have fk: "finite {0..k}" by simp
from a0 have a0r0: "a\$0 = ?r\$0" by simp
{fix n have "a \$ n = ?r \$ n"
proof(induct n rule: nat_less_induct)
@@ -1767,7 +1760,7 @@
apply (rule setprod_cong, simp)
using i a0 by (simp del: replicate.simps)
also have "\<dots> = a \$ n * (?r \$ 0)^k"
-            unfolding  setprod_gen_delta[OF fK] using i by simp
+            using i by (simp add: setprod_gen_delta)
finally show ?ths .
qed
then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a \$ n * (?r \$ 0)^k"```
```--- a/src/HOL/SupInf.thy	Fri Mar 02 09:35:32 2012 +0100
+++ b/src/HOL/SupInf.thy	Fri Mar 02 09:35:33 2012 +0100
@@ -445,11 +445,9 @@
fixes x :: real
shows "max x y = Sup {x,y}"
proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+  have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff)
moreover
-  have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
+  have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)
ultimately show ?thesis by arith
qed

@@ -457,12 +455,9 @@
fixes x :: real
shows "min x y = Inf {x,y}"
proof-
-  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
-  from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"