--- a/src/HOL/Deriv.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Deriv.thy Sun Sep 18 20:33:48 2016 +0200
@@ -119,16 +119,9 @@
qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
lemma has_derivative_setsum[simp, derivative_intros]:
- assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
- shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
-proof (cases "finite I")
- case True
- from this f show ?thesis
- by induct (simp_all add: f)
-next
- case False
- then show ?thesis by simp
-qed
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F) \<Longrightarrow>
+ ((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
+ by (induct I rule: infinite_finite_induct) simp_all
lemma has_derivative_minus[simp, derivative_intros]:
"(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
@@ -360,28 +353,24 @@
lemma has_derivative_setprod[simp, derivative_intros]:
fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
- assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
- shows "((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
-proof (cases "finite I")
- case True
- from this f show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case (insert i I)
- let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
- have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
- using insert by (intro has_derivative_mult) auto
- also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
- using insert(1,2)
- by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong)
- finally show ?case
- using insert by simp
- qed
+ shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
+ ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
+proof (induct I rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
+next
+ case empty
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case (insert i I)
+ let ?P = "\<lambda>y. f i x * (\<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x)) + (f' i y) * (\<Prod>i\<in>I. f i x)"
+ have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
+ using insert by (intro has_derivative_mult) auto
+ also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
+ using insert(1,2)
+ by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong)
+ finally show ?case
+ using insert by simp
qed
lemma has_derivative_power[simp, derivative_intros]:
--- a/src/HOL/Finite_Set.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Finite_Set.thy Sun Sep 18 20:33:48 2016 +0200
@@ -610,26 +610,22 @@
and empty: "P {}"
and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
shows "P F"
-proof -
- from \<open>finite F\<close>
- have "F \<subseteq> A \<Longrightarrow> ?thesis"
- proof induct
- show "P {}" by fact
- next
- fix x F
- assume "finite F" and "x \<notin> F" and
- P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
- show "P (insert x F)"
- proof (rule insert)
- from i show "x \<in> A" by blast
- from i have "F \<subseteq> A" by blast
- with P show "P F" .
- show "finite F" by fact
- show "x \<notin> F" by fact
- show "F \<subseteq> A" by fact
- qed
+ using assms(1,2)
+proof induct
+ show "P {}" by fact
+next
+ fix x F
+ assume "finite F" and "x \<notin> F" and
+ P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
+ show "P (insert x F)"
+ proof (rule insert)
+ from i show "x \<in> A" by blast
+ from i have "F \<subseteq> A" by blast
+ with P show "P F" .
+ show "finite F" by fact
+ show "x \<notin> F" by fact
+ show "F \<subseteq> A" by fact
qed
- with \<open>F \<subseteq> A\<close> show ?thesis by blast
qed
@@ -1442,6 +1438,7 @@
assumes "finite B"
and "B \<subseteq> A"
shows "card (A - B) = card A - card B"
+ using assms
proof (cases "finite A")
case False
with assms show ?thesis
@@ -1752,20 +1749,12 @@
lemma card_image_le: "finite A \<Longrightarrow> card (f ` A) \<le> card A"
by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
-lemma card_image:
- assumes "inj_on f A"
- shows "card (f ` A) = card A"
-proof (cases "finite A")
- case True
- then show ?thesis
- using assms by (induct A) simp_all
-next
- case False
- then have "\<not> finite (f ` A)"
- using assms by (auto dest: finite_imageD)
- with False show ?thesis
- by simp
-qed
+lemma card_image: "inj_on f A \<Longrightarrow> card (f ` A) = card A"
+proof (induct A rule: infinite_finite_induct)
+ case (infinite A)
+ then have "\<not> finite (f ` A)" by (auto dest: finite_imageD)
+ with infinite show ?case by simp
+qed simp_all
lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
by (auto simp: card_image bij_betw_def)
--- a/src/HOL/GCD.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/GCD.thy Sun Sep 18 20:33:48 2016 +0200
@@ -860,10 +860,7 @@
by (subst add_commute) simp
lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
- apply (cases "finite A")
- apply (induct set: finite)
- apply (auto simp add: gcd_mult_cancel)
- done
+ by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
by (induct xs) (simp_all add: gcd_mult_cancel)
--- a/src/HOL/Groups_Big.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Groups_Big.thy Sun Sep 18 20:33:48 2016 +0200
@@ -570,22 +570,8 @@
qed
lemma (in ordered_comm_monoid_add) setsum_mono:
- assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i"
- shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
-proof (cases "finite K")
- case True
- from this le show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case insert
- then show ?case using add_mono by fastforce
- qed
-next
- case False
- then show ?thesis by simp
-qed
+ "(\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
+ by (induct K rule: infinite_finite_induct) (use add_mono in auto)
lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono:
assumes "finite A" "A \<noteq> {}"
@@ -640,13 +626,7 @@
lemma setsum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)"
for f :: "'b \<Rightarrow> 'a::ab_group_add"
-proof (cases "finite A")
- case True
- then show ?thesis by (induct set: finite) auto
-next
- case False
- then show ?thesis by simp
-qed
+ by (induct A rule: infinite_finite_induct) auto
lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
for f g :: "'b \<Rightarrow>'a::ab_group_add"
@@ -660,43 +640,30 @@
context ordered_comm_monoid_add
begin
-lemma setsum_nonneg:
- assumes nn: "\<forall>x\<in>A. 0 \<le> f x"
- shows "0 \<le> setsum f A"
-proof (cases "finite A")
- case True
- then show ?thesis
- using nn
- proof induct
- case empty
- then show ?case by simp
- next
- case (insert x F)
- then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
- with insert show ?case by simp
- qed
+lemma setsum_nonneg: "\<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> 0 \<le> setsum f A"
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case (insert x F)
+ then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
+ with insert show ?case by simp
qed
-lemma setsum_nonpos:
- assumes np: "\<forall>x\<in>A. f x \<le> 0"
- shows "setsum f A \<le> 0"
-proof (cases "finite A")
- case True
- then show ?thesis
- using np
- proof induct
- case empty
- then show ?case by simp
- next
- case (insert x F)
- then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
- with insert show ?case by simp
- qed
+lemma setsum_nonpos: "\<forall>x\<in>A. f x \<le> 0 \<Longrightarrow> setsum f A \<le> 0"
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False thus ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case (insert x F)
+ then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
+ with insert show ?case by simp
qed
lemma setsum_nonneg_eq_0_iff:
@@ -762,73 +729,56 @@
"finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)"
by (intro ballI setsum_nonneg_eq_0_iff zero_le)
-lemma setsum_right_distrib:
- fixes f :: "'a \<Rightarrow> 'b::semiring_0"
- shows "r * setsum f A = setsum (\<lambda>n. r * f n) A"
-proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case insert
- then show ?case by (simp add: distrib_left)
- qed
+lemma setsum_right_distrib: "r * setsum f A = setsum (\<lambda>n. r * f n) A"
+ for f :: "'a \<Rightarrow> 'b::semiring_0"
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case insert
+ then show ?case by (simp add: distrib_left)
qed
lemma setsum_left_distrib: "setsum f A * r = (\<Sum>n\<in>A. f n * r)"
for r :: "'a::semiring_0"
-proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case insert
- then show ?case by (simp add: distrib_right)
- qed
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case insert
+ then show ?case by (simp add: distrib_right)
qed
lemma setsum_divide_distrib: "setsum f A / r = (\<Sum>n\<in>A. f n / r)"
for r :: "'a::field"
-proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case insert
- then show ?case by (simp add: add_divide_distrib)
- qed
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case insert
+ then show ?case by (simp add: add_divide_distrib)
qed
lemma setsum_abs[iff]: "\<bar>setsum f A\<bar> \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A"
for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
-proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case insert
- then show ?case by (auto intro: abs_triangle_ineq order_trans)
- qed
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case empty
+ then show ?case by simp
+next
+ case insert
+ then show ?case by (auto intro: abs_triangle_ineq order_trans)
qed
lemma setsum_abs_ge_zero[iff]: "0 \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A"
@@ -837,23 +787,19 @@
lemma abs_setsum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
-proof (cases "finite A")
- case True
- then show ?thesis
- proof induct
- case empty
- then show ?case by simp
- next
- case (insert a A)
- then have "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
- also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
- also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
- also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
- finally show ?case .
- qed
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
+next
+ case empty
+ then show ?case by simp
next
- case False
- then show ?thesis by simp
+ case (insert a A)
+ then have "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
+ also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
+ also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
+ also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
+ finally show ?case .
qed
lemma setsum_diff1_ring:
@@ -873,21 +819,12 @@
setsum f A * setsum g B = setsum id {f a * g b |a b. a \<in> A \<and> b \<in> B}"
by(auto simp: setsum_product setsum.cartesian_product intro!: setsum.reindex_cong[symmetric])
-lemma setsum_SucD:
- assumes "setsum f A = Suc n"
- shows "\<exists>a\<in>A. 0 < f a"
-proof (cases "finite A")
- case True
- from this assms show ?thesis by induct auto
-next
- case False
- with assms show ?thesis by simp
-qed
+lemma setsum_SucD: "setsum f A = Suc n \<Longrightarrow> \<exists>a\<in>A. 0 < f a"
+ by (induct A rule: infinite_finite_induct) auto
lemma setsum_eq_Suc0_iff:
- assumes "finite A"
- shows "setsum f A = Suc 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = Suc 0 \<and> (\<forall>b\<in>A. a \<noteq> b \<longrightarrow> f b = 0))"
- using assms by induct (auto simp add:add_is_1)
+ "finite A \<Longrightarrow> setsum f A = Suc 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = Suc 0 \<and> (\<forall>b\<in>A. a \<noteq> b \<longrightarrow> f b = 0))"
+ by (induct A rule: finite_induct) (auto simp add: add_is_1)
lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
@@ -899,17 +836,19 @@
lemma setsum_diff1_nat: "setsum f (A - {a}) = (if a \<in> A then setsum f A - f a else setsum f A)"
for f :: "'a \<Rightarrow> nat"
-proof (cases "finite A")
- case True
- then show ?thesis
- apply induct
- apply (auto simp: insert_Diff_if)
+proof (induct A rule: infinite_finite_induct)
+ case infinite
+ then show ?case by simp
+next
+ case empty
+ then show ?case by simp
+next
+ case insert
+ then show ?case
+ apply (auto simp: insert_Diff_if)
apply (drule mk_disjoint_insert)
apply auto
done
-next
- case False
- then show ?thesis by simp
qed
lemma setsum_diff_nat:
@@ -941,15 +880,8 @@
qed
lemma setsum_comp_morphism:
- assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
- shows "setsum (h \<circ> g) A = h (setsum g A)"
-proof (cases "finite A")
- case False
- then show ?thesis by (simp add: assms)
-next
- case True
- then show ?thesis by (induct A) (simp_all add: assms)
-qed
+ "h 0 = 0 \<Longrightarrow> (\<And>x y. h (x + y) = h x + h y) \<Longrightarrow> setsum (h \<circ> g) A = h (setsum g A)"
+ by (induct A rule: infinite_finite_induct) simp_all
lemma (in comm_semiring_1) dvd_setsum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
by (induct A rule: infinite_finite_induct) simp_all
@@ -995,13 +927,7 @@
qed
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
-proof (cases "finite A")
- case True
- then show ?thesis by induct (auto simp: algebra_simps)
-next
- case False
- then show ?thesis by simp
-qed
+ by (induct A rule: infinite_finite_induct) (auto simp: algebra_simps)
lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
using setsum.distrib[of f "\<lambda>_. 1" A] by simp
@@ -1033,7 +959,7 @@
proof (cases "finite A")
case True
then show ?thesis
- using le setsum_mono[where K=A and f = "%x. K"] by simp
+ using le setsum_mono[where K=A and f = "\<lambda>x. K"] by simp
next
case False
then show ?thesis by simp
--- a/src/HOL/Lattices_Big.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Lattices_Big.thy Sun Sep 18 20:33:48 2016 +0200
@@ -522,9 +522,11 @@
assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
shows "Min (insert a A) = a"
proof (cases "A = {}")
- case True then show ?thesis by simp
+ case True
+ then show ?thesis by simp
next
- case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
+ case False
+ with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
by simp
moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
ultimately show ?thesis by (simp add: min.absorb1)
@@ -534,9 +536,11 @@
assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
shows "Max (insert a A) = a"
proof (cases "A = {}")
- case True then show ?thesis by simp
+ case True
+ then show ?thesis by simp
next
- case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
+ case False
+ with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
by simp
moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
ultimately show ?thesis by (simp add: max.absorb1)
--- a/src/HOL/Limits.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Limits.thy Sun Sep 18 20:33:48 2016 +0200
@@ -643,17 +643,8 @@
lemma tendsto_setsum [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
- assumes "\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
- shows "((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
-proof (cases "finite I")
- case True
- then show ?thesis
- using assms by induct (simp_all add: tendsto_add)
-next
- case False
- then show ?thesis
- by simp
-qed
+ shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
+ by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)
lemma continuous_setsum [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
@@ -844,16 +835,8 @@
lemma tendsto_setprod [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F"
- shows "((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F"
-proof (cases "finite S")
- case True
- then show ?thesis using assms
- by induct (simp_all add: tendsto_mult)
-next
- case False
- then show ?thesis by simp
-qed
+ shows "(\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F"
+ by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)
lemma continuous_setprod [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
@@ -1905,17 +1888,8 @@
lemma convergent_setsum:
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
- assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
- shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
-proof (cases "finite A")
- case True
- then show ?thesis
- using assms by (induct A set: finite) (simp_all add: convergent_const convergent_add)
-next
- case False
- then show ?thesis
- by (simp add: convergent_const)
-qed
+ shows "(\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)) \<Longrightarrow> convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+ by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add)
lemma (in bounded_linear) convergent:
assumes "convergent (\<lambda>n. X n)"
--- a/src/HOL/Real_Vector_Spaces.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Sep 18 20:33:48 2016 +0200
@@ -34,12 +34,7 @@
using add [of x "- y"] by (simp add: minus)
lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
- apply (cases "finite A")
- apply (induct set: finite)
- apply (simp add: zero)
- apply (simp add: add)
- apply (simp add: zero)
- done
+ by (induct A rule: infinite_finite_induct) (simp_all add: zero add)
end
@@ -223,10 +218,7 @@
lemma setsum_constant_scaleR: "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
for y :: "'a::real_vector"
- apply (cases "finite A")
- apply (induct set: finite)
- apply (simp_all add: algebra_simps)
- done
+ by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
lemma vector_add_divide_simps:
"v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
@@ -475,31 +467,17 @@
then show thesis ..
qed
-lemma setsum_in_Reals [intro,simp]:
- assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>"
- shows "setsum f s \<in> \<real>"
-proof (cases "finite s")
- case True
- then show ?thesis
- using assms by (induct s rule: finite_induct) auto
-next
- case False
- then show ?thesis
- using assms by (metis Reals_0 setsum.infinite)
-qed
+lemma setsum_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setsum f s \<in> \<real>"
+proof (induct s rule: infinite_finite_induct)
+ case infinite
+ then show ?case by (metis Reals_0 setsum.infinite)
+qed simp_all
-lemma setprod_in_Reals [intro,simp]:
- assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>"
- shows "setprod f s \<in> \<real>"
-proof (cases "finite s")
- case True
- then show ?thesis
- using assms by (induct s rule: finite_induct) auto
-next
- case False
- then show ?thesis
- using assms by (metis Reals_1 setprod.infinite)
-qed
+lemma setprod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setprod f s \<in> \<real>"
+proof (induct s rule: infinite_finite_induct)
+ case infinite
+ then show ?case by (metis Reals_1 setprod.infinite)
+qed simp_all
lemma Reals_induct [case_names of_real, induct set: Reals]:
"q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
@@ -1572,16 +1550,8 @@
lemma bounded_linear_setsum:
fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes "\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)"
- shows "bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
-proof (cases "finite I")
- case True
- then show ?thesis
- using assms by induct (auto intro!: bounded_linear_add)
-next
- case False
- then show ?thesis by simp
-qed
+ shows "(\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)) \<Longrightarrow> bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
+ by (induct I rule: infinite_finite_induct) (auto intro!: bounded_linear_add)
lemma bounded_linear_compose:
assumes "bounded_linear f"
--- a/src/HOL/Set_Interval.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Set_Interval.thy Sun Sep 18 20:33:48 2016 +0200
@@ -936,7 +936,7 @@
"Suc ` {..<n} = {1..n}"
using image_add_atLeastLessThan [of 1 0 n]
by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
-
+
corollary image_Suc_atMost:
"Suc ` {..n} = {1..Suc n}"
using image_add_atLeastLessThan [of 1 0 "Suc n"]
@@ -1198,13 +1198,13 @@
lemma subset_eq_atLeast0_lessThan_finite:
fixes n :: nat
assumes "N \<subseteq> {0..<n}"
- shows "finite N"
+ shows "finite N"
using assms finite_atLeastLessThan by (rule finite_subset)
lemma subset_eq_atLeast0_atMost_finite:
fixes n :: nat
assumes "N \<subseteq> {0..n}"
- shows "finite N"
+ shows "finite N"
using assms finite_atLeastAtMost by (rule finite_subset)
lemma ex_bij_betw_nat_finite:
@@ -1992,7 +1992,7 @@
proof
assume "m \<in> ?A"
with assms show "m \<in> ?B"
- by auto
+ by auto
next
assume "m \<in> ?B"
moreover have "m mod n \<in> ?A"
--- a/src/HOL/Wellfounded.thy Sun Sep 18 17:59:28 2016 +0200
+++ b/src/HOL/Wellfounded.thy Sun Sep 18 20:33:48 2016 +0200
@@ -790,61 +790,55 @@
assumes wf: "wf r"
shows "wf (max_ext r)"
proof (rule acc_wfI, intro allI)
- fix M
- show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
- proof (cases "finite M")
- case True
- then show ?thesis
- proof (induct M)
- case empty
- show ?case
- by (rule accI) (auto elim: max_ext.cases)
- next
- case (insert a M)
- from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
- proof (induct arbitrary: M)
- fix M a
- assume "M \<in> ?W"
- assume [intro]: "finite M"
- assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
- have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
- if "finite N" "finite M" for N M :: "'a set"
- using that by (induct N arbitrary: M) (auto simp: hyp)
- show "insert a M \<in> ?W"
- proof (rule accI)
- fix N
- assume Nless: "(N, insert a M) \<in> max_ext r"
- then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
- by (auto elim!: max_ext.cases)
+ show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M
+ proof (induct M rule: infinite_finite_induct)
+ case empty
+ show ?case
+ by (rule accI) (auto elim: max_ext.cases)
+ next
+ case (insert a M)
+ from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
+ proof (induct arbitrary: M)
+ fix M a
+ assume "M \<in> ?W"
+ assume [intro]: "finite M"
+ assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
+ have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
+ if "finite N" "finite M" for N M :: "'a set"
+ using that by (induct N arbitrary: M) (auto simp: hyp)
+ show "insert a M \<in> ?W"
+ proof (rule accI)
+ fix N
+ assume Nless: "(N, insert a M) \<in> max_ext r"
+ then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
+ by (auto elim!: max_ext.cases)
- let ?N1 = "{n \<in> N. (n, a) \<in> r}"
- let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
- have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
- from Nless have "finite N" by (auto elim: max_ext.cases)
- then have finites: "finite ?N1" "finite ?N2" by auto
+ let ?N1 = "{n \<in> N. (n, a) \<in> r}"
+ let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
+ have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
+ from Nless have "finite N" by (auto elim: max_ext.cases)
+ then have finites: "finite ?N1" "finite ?N2" by auto
- have "?N2 \<in> ?W"
- proof (cases "M = {}")
- case [simp]: True
- have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
- from * have "?N2 = {}" by auto
- with Mw show "?N2 \<in> ?W" by (simp only:)
- next
- case False
- from * finites have N2: "(?N2, M) \<in> max_ext r"
- by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
- with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
- qed
- with finites have "?N1 \<union> ?N2 \<in> ?W"
- by (rule add_less) simp
- then show "N \<in> ?W" by (simp only: N)
+ have "?N2 \<in> ?W"
+ proof (cases "M = {}")
+ case [simp]: True
+ have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
+ from * have "?N2 = {}" by auto
+ with Mw show "?N2 \<in> ?W" by (simp only:)
+ next
+ case False
+ from * finites have N2: "(?N2, M) \<in> max_ext r"
+ by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
+ with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
qed
+ with finites have "?N1 \<union> ?N2 \<in> ?W"
+ by (rule add_less) simp
+ then show "N \<in> ?W" by (simp only: N)
qed
qed
next
- case [simp]: False
- show ?thesis
- by (rule accI) (auto elim: max_ext.cases)
+ case [simp]: infinite
+ show ?case by (rule accI) (auto elim: max_ext.cases)
qed
qed