# HG changeset patch # User bulwahn # Date 1330677333 -3600 # Node ID ad878aff9c15e2b13366ae7c04cb1e52e404849a # Parent faf62905cd534b0de612d68365b70ce8b8f5bd51 removing finiteness goals diff -r faf62905cd53 -r ad878aff9c15 src/HOL/Library/Binomial.thy --- 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} \ {Suc n} = {}" by auto have eq: "{0..Suc n} = {0..n} \ {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} \ {1.. Suc n} = {}" by auto have eq: "{0..Suc n} = {0} \ {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 diff -r faf62905cd53 -r ad878aff9c15 src/HOL/Library/Formal_Power_Series.thy --- 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 \ 0" - have fN: "finite {0 .. n}" by simp have "(X * f) $n = (\i = 0..n. X $ i * f $ (n - i))" by (simp add: fps_mult_nth) also have "\ = 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} \ {1 .. n}" by auto have d: "{0} \ {1 .. n} = {}" by auto - have f: "finite {0::nat}" "finite {1..n}" by auto from f0 np have th0: "- (inverse f$n) = (setsum (\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 "\ = f$0 * natfun_inverse f n + (\i = 1..n. f$i * natfun_inverse f (n-i))" - unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] - by simp + by (simp add: eq) also have "\ = 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 (\v. setprod (\j. a $ (v!j)) {0..m}) (natpermute n (m+1))" proof- - have f: "finite {0 ..m}" by simp - have th0: "a^Suc m = setprod (\i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp + have th0: "a^Suc m = setprod (\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 = (\j\{0..h}. fps_radical r k a $ (replicate k 0) ! j)" unfolding fps_power_nth h by simp also have "\ = (\j\{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 "\ = 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 \ 0" using n1 by arith let ?Pnk = "natpermute n (k + 1)" let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" @@ -1639,7 +1633,7 @@ apply (rule setprod_cong, simp) using i r0 by (simp del: replicate.simps) also have "\ = (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 "\ = 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" diff -r faf62905cd53 -r ad878aff9c15 src/HOL/SupInf.thy --- 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} \ {}" by simp_all - from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \ max x y" by simp + have "Sup {x,y} \ max x y" by (simp add: Sup_finite_le_iff) moreover - have "max x y \ Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"] - by (simp add: linorder_linear) + have "max x y \ 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} \ {}" by simp_all - from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \ min x y" - by (simp add: linorder_linear) + have "Inf {x,y} \ min x y" by (simp add: linorder_linear Inf_finite_le_iff) moreover - have "min x y \ Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"] - by simp + have "min x y \ Inf {x,y}" by (simp add: Inf_finite_ge_iff) ultimately show ?thesis by arith qed