# HG changeset patch
# User wenzelm
# Date 1474225584 -7200
# Node ID 5e816da75b8f87731ba40c18fc5cf1eb3f49192c
# Parent  255294779d401332a9ee55df0c09d1a4692a82e7# Parent  bab633745c7fd4dbf6eafc66a3d886f5c1618735
merged

diff -r 255294779d40 -r 5e816da75b8f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Deriv.thy	Sun Sep 18 21:06:24 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]:
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Sep 18 21:06:24 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)
diff -r 255294779d40 -r 5e816da75b8f src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/GCD.thy	Sun Sep 18 21:06:24 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)
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Sep 18 21:06:24 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
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Lattices_Big.thy	Sun Sep 18 21:06:24 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)
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Limits.thy	Sun Sep 18 21:06:24 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)"
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Sun Sep 18 21:06:24 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"
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Sun Sep 18 21:06:24 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"
diff -r 255294779d40 -r 5e816da75b8f src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Sep 18 18:36:37 2016 +0200
+++ b/src/HOL/Wellfounded.thy	Sun Sep 18 21:06:24 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