tuned proofs;
authorwenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915bab633745c7f
parent 63912 9f8325206465
child 63916 5e816da75b8f
tuned proofs;
src/HOL/Deriv.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Groups_Big.thy
src/HOL/Lattices_Big.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Deriv.thy	Sun Sep 18 17:59:28 2016 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Sun Sep 18 20:33:48 2016 +0200
     1.3 @@ -119,16 +119,9 @@
     1.4  qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear)
     1.5  
     1.6  lemma has_derivative_setsum[simp, derivative_intros]:
     1.7 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F"
     1.8 -  shows "((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
     1.9 -proof (cases "finite I")
    1.10 -  case True
    1.11 -  from this f show ?thesis
    1.12 -    by induct (simp_all add: f)
    1.13 -next
    1.14 -  case False
    1.15 -  then show ?thesis by simp
    1.16 -qed
    1.17 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) F) \<Longrightarrow>
    1.18 +    ((\<lambda>x. \<Sum>i\<in>I. f i x) has_derivative (\<lambda>x. \<Sum>i\<in>I. f' i x)) F"
    1.19 +  by (induct I rule: infinite_finite_induct) simp_all
    1.20  
    1.21  lemma has_derivative_minus[simp, derivative_intros]:
    1.22    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. - f x) has_derivative (\<lambda>x. - f' x)) F"
    1.23 @@ -360,28 +353,24 @@
    1.24  
    1.25  lemma has_derivative_setprod[simp, derivative_intros]:
    1.26    fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
    1.27 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)"
    1.28 -  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)"
    1.29 -proof (cases "finite I")
    1.30 -  case True
    1.31 -  from this f show ?thesis
    1.32 -  proof induct
    1.33 -    case empty
    1.34 -    then show ?case by simp
    1.35 -  next
    1.36 -    case (insert i I)
    1.37 -    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)"
    1.38 -    have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
    1.39 -      using insert by (intro has_derivative_mult) auto
    1.40 -    also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
    1.41 -      using insert(1,2)
    1.42 -      by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong)
    1.43 -    finally show ?case
    1.44 -      using insert by simp
    1.45 -  qed
    1.46 +  shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
    1.47 +    ((\<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)"
    1.48 +proof (induct I rule: infinite_finite_induct)
    1.49 +  case infinite
    1.50 +  then show ?case by simp
    1.51 +next
    1.52 +  case empty
    1.53 +  then show ?case by simp
    1.54  next
    1.55 -  case False
    1.56 -  then show ?thesis by simp
    1.57 +  case (insert i I)
    1.58 +  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)"
    1.59 +  have "((\<lambda>x. f i x * (\<Prod>i\<in>I. f i x)) has_derivative ?P) (at x within s)"
    1.60 +    using insert by (intro has_derivative_mult) auto
    1.61 +  also have "?P = (\<lambda>y. \<Sum>i'\<in>insert i I. f' i' y * (\<Prod>j\<in>insert i I - {i'}. f j x))"
    1.62 +    using insert(1,2)
    1.63 +    by (auto simp add: setsum_right_distrib insert_Diff_if intro!: ext setsum.cong)
    1.64 +  finally show ?case
    1.65 +    using insert by simp
    1.66  qed
    1.67  
    1.68  lemma has_derivative_power[simp, derivative_intros]:
     2.1 --- a/src/HOL/Finite_Set.thy	Sun Sep 18 17:59:28 2016 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sun Sep 18 20:33:48 2016 +0200
     2.3 @@ -610,26 +610,22 @@
     2.4      and empty: "P {}"
     2.5      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)"
     2.6    shows "P F"
     2.7 -proof -
     2.8 -  from \<open>finite F\<close>
     2.9 -  have "F \<subseteq> A \<Longrightarrow> ?thesis"
    2.10 -  proof induct
    2.11 -    show "P {}" by fact
    2.12 -  next
    2.13 -    fix x F
    2.14 -    assume "finite F" and "x \<notin> F" and
    2.15 -      P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
    2.16 -    show "P (insert x F)"
    2.17 -    proof (rule insert)
    2.18 -      from i show "x \<in> A" by blast
    2.19 -      from i have "F \<subseteq> A" by blast
    2.20 -      with P show "P F" .
    2.21 -      show "finite F" by fact
    2.22 -      show "x \<notin> F" by fact
    2.23 -      show "F \<subseteq> A" by fact
    2.24 -    qed
    2.25 +  using assms(1,2)
    2.26 +proof induct
    2.27 +  show "P {}" by fact
    2.28 +next
    2.29 +  fix x F
    2.30 +  assume "finite F" and "x \<notin> F" and
    2.31 +    P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
    2.32 +  show "P (insert x F)"
    2.33 +  proof (rule insert)
    2.34 +    from i show "x \<in> A" by blast
    2.35 +    from i have "F \<subseteq> A" by blast
    2.36 +    with P show "P F" .
    2.37 +    show "finite F" by fact
    2.38 +    show "x \<notin> F" by fact
    2.39 +    show "F \<subseteq> A" by fact
    2.40    qed
    2.41 -  with \<open>F \<subseteq> A\<close> show ?thesis by blast
    2.42  qed
    2.43  
    2.44  
    2.45 @@ -1442,6 +1438,7 @@
    2.46    assumes "finite B"
    2.47      and "B \<subseteq> A"
    2.48    shows "card (A - B) = card A - card B"
    2.49 +  using assms
    2.50  proof (cases "finite A")
    2.51    case False
    2.52    with assms show ?thesis
    2.53 @@ -1752,20 +1749,12 @@
    2.54  lemma card_image_le: "finite A \<Longrightarrow> card (f ` A) \<le> card A"
    2.55    by (induct rule: finite_induct) (simp_all add: le_SucI card_insert_if)
    2.56  
    2.57 -lemma card_image:
    2.58 -  assumes "inj_on f A"
    2.59 -  shows "card (f ` A) = card A"
    2.60 -proof (cases "finite A")
    2.61 -  case True
    2.62 -  then show ?thesis
    2.63 -    using assms by (induct A) simp_all
    2.64 -next
    2.65 -  case False
    2.66 -  then have "\<not> finite (f ` A)"
    2.67 -    using assms by (auto dest: finite_imageD)
    2.68 -  with False show ?thesis
    2.69 -    by simp
    2.70 -qed
    2.71 +lemma card_image: "inj_on f A \<Longrightarrow> card (f ` A) = card A"
    2.72 +proof (induct A rule: infinite_finite_induct)
    2.73 +  case (infinite A)
    2.74 +  then have "\<not> finite (f ` A)" by (auto dest: finite_imageD)
    2.75 +  with infinite show ?case by simp
    2.76 +qed simp_all
    2.77  
    2.78  lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
    2.79    by (auto simp: card_image bij_betw_def)
     3.1 --- a/src/HOL/GCD.thy	Sun Sep 18 17:59:28 2016 +0200
     3.2 +++ b/src/HOL/GCD.thy	Sun Sep 18 20:33:48 2016 +0200
     3.3 @@ -860,10 +860,7 @@
     3.4    by (subst add_commute) simp
     3.5  
     3.6  lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
     3.7 -  apply (cases "finite A")
     3.8 -   apply (induct set: finite)
     3.9 -    apply (auto simp add: gcd_mult_cancel)
    3.10 -  done
    3.11 +  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
    3.12  
    3.13  lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
    3.14    by (induct xs) (simp_all add: gcd_mult_cancel)
     4.1 --- a/src/HOL/Groups_Big.thy	Sun Sep 18 17:59:28 2016 +0200
     4.2 +++ b/src/HOL/Groups_Big.thy	Sun Sep 18 20:33:48 2016 +0200
     4.3 @@ -570,22 +570,8 @@
     4.4  qed
     4.5  
     4.6  lemma (in ordered_comm_monoid_add) setsum_mono:
     4.7 -  assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i"
     4.8 -  shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
     4.9 -proof (cases "finite K")
    4.10 -  case True
    4.11 -  from this le show ?thesis
    4.12 -  proof induct
    4.13 -    case empty
    4.14 -    then show ?case by simp
    4.15 -  next
    4.16 -    case insert
    4.17 -    then show ?case using add_mono by fastforce
    4.18 -  qed
    4.19 -next
    4.20 -  case False
    4.21 -  then show ?thesis by simp
    4.22 -qed
    4.23 +  "(\<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)"
    4.24 +  by (induct K rule: infinite_finite_induct) (use add_mono in auto)
    4.25  
    4.26  lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono:
    4.27    assumes "finite A" "A \<noteq> {}"
    4.28 @@ -640,13 +626,7 @@
    4.29  
    4.30  lemma setsum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)"
    4.31    for f :: "'b \<Rightarrow> 'a::ab_group_add"
    4.32 -proof (cases "finite A")
    4.33 -  case True
    4.34 -  then show ?thesis by (induct set: finite) auto
    4.35 -next
    4.36 -  case False
    4.37 -  then show ?thesis by simp
    4.38 -qed
    4.39 +  by (induct A rule: infinite_finite_induct) auto
    4.40  
    4.41  lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
    4.42    for f g :: "'b \<Rightarrow>'a::ab_group_add"
    4.43 @@ -660,43 +640,30 @@
    4.44  context ordered_comm_monoid_add
    4.45  begin
    4.46  
    4.47 -lemma setsum_nonneg:
    4.48 -  assumes nn: "\<forall>x\<in>A. 0 \<le> f x"
    4.49 -  shows "0 \<le> setsum f A"
    4.50 -proof (cases "finite A")
    4.51 -  case True
    4.52 -  then show ?thesis
    4.53 -    using nn
    4.54 -  proof induct
    4.55 -    case empty
    4.56 -    then show ?case by simp
    4.57 -  next
    4.58 -    case (insert x F)
    4.59 -    then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
    4.60 -    with insert show ?case by simp
    4.61 -  qed
    4.62 +lemma setsum_nonneg: "\<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> 0 \<le> setsum f A"
    4.63 +proof (induct A rule: infinite_finite_induct)
    4.64 +  case infinite
    4.65 +  then show ?case by simp
    4.66  next
    4.67 -  case False
    4.68 -  then show ?thesis by simp
    4.69 +  case empty
    4.70 +  then show ?case by simp
    4.71 +next
    4.72 +  case (insert x F)
    4.73 +  then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
    4.74 +  with insert show ?case by simp
    4.75  qed
    4.76  
    4.77 -lemma setsum_nonpos:
    4.78 -  assumes np: "\<forall>x\<in>A. f x \<le> 0"
    4.79 -  shows "setsum f A \<le> 0"
    4.80 -proof (cases "finite A")
    4.81 -  case True
    4.82 -  then show ?thesis
    4.83 -    using np
    4.84 -  proof induct
    4.85 -    case empty
    4.86 -    then show ?case by simp
    4.87 -  next
    4.88 -    case (insert x F)
    4.89 -    then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
    4.90 -    with insert show ?case by simp
    4.91 -  qed
    4.92 +lemma setsum_nonpos: "\<forall>x\<in>A. f x \<le> 0 \<Longrightarrow> setsum f A \<le> 0"
    4.93 +proof (induct A rule: infinite_finite_induct)
    4.94 +  case infinite
    4.95 +  then show ?case by simp
    4.96  next
    4.97 -  case False thus ?thesis by simp
    4.98 +  case empty
    4.99 +  then show ?case by simp
   4.100 +next
   4.101 +  case (insert x F)
   4.102 +  then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   4.103 +  with insert show ?case by simp
   4.104  qed
   4.105  
   4.106  lemma setsum_nonneg_eq_0_iff:
   4.107 @@ -762,73 +729,56 @@
   4.108    "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)"
   4.109    by (intro ballI setsum_nonneg_eq_0_iff zero_le)
   4.110  
   4.111 -lemma setsum_right_distrib:
   4.112 -  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   4.113 -  shows "r * setsum f A = setsum (\<lambda>n. r * f n) A"
   4.114 -proof (cases "finite A")
   4.115 -  case True
   4.116 -  then show ?thesis
   4.117 -  proof induct
   4.118 -    case empty
   4.119 -    then show ?case by simp
   4.120 -  next
   4.121 -    case insert
   4.122 -    then show ?case by (simp add: distrib_left)
   4.123 -  qed
   4.124 +lemma setsum_right_distrib: "r * setsum f A = setsum (\<lambda>n. r * f n) A"
   4.125 +  for f :: "'a \<Rightarrow> 'b::semiring_0"
   4.126 +proof (induct A rule: infinite_finite_induct)
   4.127 +  case infinite
   4.128 +  then show ?case by simp
   4.129  next
   4.130 -  case False
   4.131 -  then show ?thesis by simp
   4.132 +  case empty
   4.133 +  then show ?case by simp
   4.134 +next
   4.135 +  case insert
   4.136 +  then show ?case by (simp add: distrib_left)
   4.137  qed
   4.138  
   4.139  lemma setsum_left_distrib: "setsum f A * r = (\<Sum>n\<in>A. f n * r)"
   4.140    for r :: "'a::semiring_0"
   4.141 -proof (cases "finite A")
   4.142 -  case True
   4.143 -  then show ?thesis
   4.144 -  proof induct
   4.145 -    case empty
   4.146 -    then show ?case by simp
   4.147 -  next
   4.148 -    case insert
   4.149 -    then show ?case by (simp add: distrib_right)
   4.150 -  qed
   4.151 +proof (induct A rule: infinite_finite_induct)
   4.152 +  case infinite
   4.153 +  then show ?case by simp
   4.154  next
   4.155 -  case False
   4.156 -  then show ?thesis by simp
   4.157 +  case empty
   4.158 +  then show ?case by simp
   4.159 +next
   4.160 +  case insert
   4.161 +  then show ?case by (simp add: distrib_right)
   4.162  qed
   4.163  
   4.164  lemma setsum_divide_distrib: "setsum f A / r = (\<Sum>n\<in>A. f n / r)"
   4.165    for r :: "'a::field"
   4.166 -proof (cases "finite A")
   4.167 -  case True
   4.168 -  then show ?thesis
   4.169 -  proof induct
   4.170 -    case empty
   4.171 -    then show ?case by simp
   4.172 -  next
   4.173 -    case insert
   4.174 -    then show ?case by (simp add: add_divide_distrib)
   4.175 -  qed
   4.176 +proof (induct A rule: infinite_finite_induct)
   4.177 +  case infinite
   4.178 +  then show ?case by simp
   4.179  next
   4.180 -  case False
   4.181 -  then show ?thesis by simp
   4.182 +  case empty
   4.183 +  then show ?case by simp
   4.184 +next
   4.185 +  case insert
   4.186 +  then show ?case by (simp add: add_divide_distrib)
   4.187  qed
   4.188  
   4.189  lemma setsum_abs[iff]: "\<bar>setsum f A\<bar> \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A"
   4.190    for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   4.191 -proof (cases "finite A")
   4.192 -  case True
   4.193 -  then show ?thesis
   4.194 -  proof induct
   4.195 -    case empty
   4.196 -    then show ?case by simp
   4.197 -  next
   4.198 -    case insert
   4.199 -    then show ?case by (auto intro: abs_triangle_ineq order_trans)
   4.200 -  qed
   4.201 +proof (induct A rule: infinite_finite_induct)
   4.202 +  case infinite
   4.203 +  then show ?case by simp
   4.204  next
   4.205 -  case False
   4.206 -  then show ?thesis by simp
   4.207 +  case empty
   4.208 +  then show ?case by simp
   4.209 +next
   4.210 +  case insert
   4.211 +  then show ?case by (auto intro: abs_triangle_ineq order_trans)
   4.212  qed
   4.213  
   4.214  lemma setsum_abs_ge_zero[iff]: "0 \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A"
   4.215 @@ -837,23 +787,19 @@
   4.216  
   4.217  lemma abs_setsum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
   4.218    for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   4.219 -proof (cases "finite A")
   4.220 -  case True
   4.221 -  then show ?thesis
   4.222 -  proof induct
   4.223 -    case empty
   4.224 -    then show ?case by simp
   4.225 -  next
   4.226 -    case (insert a A)
   4.227 -    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
   4.228 -    also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
   4.229 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
   4.230 -    also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
   4.231 -    finally show ?case .
   4.232 -  qed
   4.233 +proof (induct A rule: infinite_finite_induct)
   4.234 +  case infinite
   4.235 +  then show ?case by simp
   4.236 +next
   4.237 +  case empty
   4.238 +  then show ?case by simp
   4.239  next
   4.240 -  case False
   4.241 -  then show ?thesis by simp
   4.242 +  case (insert a A)
   4.243 +  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
   4.244 +  also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
   4.245 +  also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
   4.246 +  also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
   4.247 +  finally show ?case .
   4.248  qed
   4.249  
   4.250  lemma setsum_diff1_ring:
   4.251 @@ -873,21 +819,12 @@
   4.252      setsum f A * setsum g B = setsum id {f a * g b |a b. a \<in> A \<and> b \<in> B}"
   4.253    by(auto simp: setsum_product setsum.cartesian_product intro!: setsum.reindex_cong[symmetric])
   4.254  
   4.255 -lemma setsum_SucD:
   4.256 -  assumes "setsum f A = Suc n"
   4.257 -  shows "\<exists>a\<in>A. 0 < f a"
   4.258 -proof (cases "finite A")
   4.259 -  case True
   4.260 -  from this assms show ?thesis by induct auto
   4.261 -next
   4.262 -  case False
   4.263 -  with assms show ?thesis by simp
   4.264 -qed
   4.265 +lemma setsum_SucD: "setsum f A = Suc n \<Longrightarrow> \<exists>a\<in>A. 0 < f a"
   4.266 +  by (induct A rule: infinite_finite_induct) auto
   4.267  
   4.268  lemma setsum_eq_Suc0_iff:
   4.269 -  assumes "finite A"
   4.270 -  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))"
   4.271 -  using assms by induct (auto simp add:add_is_1)
   4.272 +  "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))"
   4.273 +  by (induct A rule: finite_induct) (auto simp add: add_is_1)
   4.274  
   4.275  lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   4.276  
   4.277 @@ -899,17 +836,19 @@
   4.278  
   4.279  lemma setsum_diff1_nat: "setsum f (A - {a}) = (if a \<in> A then setsum f A - f a else setsum f A)"
   4.280    for f :: "'a \<Rightarrow> nat"
   4.281 -proof (cases "finite A")
   4.282 -  case True
   4.283 -  then show ?thesis
   4.284 -    apply induct
   4.285 -     apply (auto simp: insert_Diff_if)
   4.286 +proof (induct A rule: infinite_finite_induct)
   4.287 +  case infinite
   4.288 +  then show ?case by simp
   4.289 +next
   4.290 +  case empty
   4.291 +  then show ?case by simp
   4.292 +next
   4.293 +  case insert
   4.294 +  then show ?case
   4.295 +    apply (auto simp: insert_Diff_if)
   4.296      apply (drule mk_disjoint_insert)
   4.297      apply auto
   4.298      done
   4.299 -next
   4.300 -  case False
   4.301 -  then show ?thesis by simp
   4.302  qed
   4.303  
   4.304  lemma setsum_diff_nat:
   4.305 @@ -941,15 +880,8 @@
   4.306  qed
   4.307  
   4.308  lemma setsum_comp_morphism:
   4.309 -  assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   4.310 -  shows "setsum (h \<circ> g) A = h (setsum g A)"
   4.311 -proof (cases "finite A")
   4.312 -  case False
   4.313 -  then show ?thesis by (simp add: assms)
   4.314 -next
   4.315 -  case True
   4.316 -  then show ?thesis by (induct A) (simp_all add: assms)
   4.317 -qed
   4.318 +  "h 0 = 0 \<Longrightarrow> (\<And>x y. h (x + y) = h x + h y) \<Longrightarrow> setsum (h \<circ> g) A = h (setsum g A)"
   4.319 +  by (induct A rule: infinite_finite_induct) simp_all
   4.320  
   4.321  lemma (in comm_semiring_1) dvd_setsum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   4.322    by (induct A rule: infinite_finite_induct) simp_all
   4.323 @@ -995,13 +927,7 @@
   4.324  qed
   4.325  
   4.326  lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   4.327 -proof (cases "finite A")
   4.328 -  case True
   4.329 -  then show ?thesis by induct (auto simp: algebra_simps)
   4.330 -next
   4.331 -  case False
   4.332 -  then show ?thesis by simp
   4.333 -qed
   4.334 +  by (induct A rule: infinite_finite_induct) (auto simp: algebra_simps)
   4.335  
   4.336  lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
   4.337    using setsum.distrib[of f "\<lambda>_. 1" A] by simp
   4.338 @@ -1033,7 +959,7 @@
   4.339  proof (cases "finite A")
   4.340    case True
   4.341    then show ?thesis
   4.342 -    using le setsum_mono[where K=A and f = "%x. K"] by simp
   4.343 +    using le setsum_mono[where K=A and f = "\<lambda>x. K"] by simp
   4.344  next
   4.345    case False
   4.346    then show ?thesis by simp
     5.1 --- a/src/HOL/Lattices_Big.thy	Sun Sep 18 17:59:28 2016 +0200
     5.2 +++ b/src/HOL/Lattices_Big.thy	Sun Sep 18 20:33:48 2016 +0200
     5.3 @@ -522,9 +522,11 @@
     5.4    assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
     5.5    shows "Min (insert a A) = a"
     5.6  proof (cases "A = {}")
     5.7 -  case True then show ?thesis by simp
     5.8 +  case True
     5.9 +  then show ?thesis by simp
    5.10  next
    5.11 -  case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
    5.12 +  case False
    5.13 +  with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
    5.14      by simp
    5.15    moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
    5.16    ultimately show ?thesis by (simp add: min.absorb1)
    5.17 @@ -534,9 +536,11 @@
    5.18    assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
    5.19    shows "Max (insert a A) = a"
    5.20  proof (cases "A = {}")
    5.21 -  case True then show ?thesis by simp
    5.22 +  case True
    5.23 +  then show ?thesis by simp
    5.24  next
    5.25 -  case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
    5.26 +  case False
    5.27 +  with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
    5.28      by simp
    5.29    moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
    5.30    ultimately show ?thesis by (simp add: max.absorb1)
     6.1 --- a/src/HOL/Limits.thy	Sun Sep 18 17:59:28 2016 +0200
     6.2 +++ b/src/HOL/Limits.thy	Sun Sep 18 20:33:48 2016 +0200
     6.3 @@ -643,17 +643,8 @@
     6.4  
     6.5  lemma tendsto_setsum [tendsto_intros]:
     6.6    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
     6.7 -  assumes "\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
     6.8 -  shows "((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
     6.9 -proof (cases "finite I")
    6.10 -  case True
    6.11 -  then show ?thesis
    6.12 -    using assms by induct (simp_all add: tendsto_add)
    6.13 -next
    6.14 -  case False
    6.15 -  then show ?thesis
    6.16 -    by simp
    6.17 -qed
    6.18 +  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"
    6.19 +  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)
    6.20  
    6.21  lemma continuous_setsum [continuous_intros]:
    6.22    fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
    6.23 @@ -844,16 +835,8 @@
    6.24  
    6.25  lemma tendsto_setprod [tendsto_intros]:
    6.26    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
    6.27 -  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F"
    6.28 -  shows "((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F"
    6.29 -proof (cases "finite S")
    6.30 -  case True
    6.31 -  then show ?thesis using assms
    6.32 -    by induct (simp_all add: tendsto_mult)
    6.33 -next
    6.34 -  case False
    6.35 -  then show ?thesis by simp
    6.36 -qed
    6.37 +  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"
    6.38 +  by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)
    6.39  
    6.40  lemma continuous_setprod [continuous_intros]:
    6.41    fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
    6.42 @@ -1905,17 +1888,8 @@
    6.43  
    6.44  lemma convergent_setsum:
    6.45    fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
    6.46 -  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
    6.47 -  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
    6.48 -proof (cases "finite A")
    6.49 -  case True
    6.50 -  then show ?thesis
    6.51 -    using assms by (induct A set: finite) (simp_all add: convergent_const convergent_add)
    6.52 -next
    6.53 -  case False
    6.54 -  then show ?thesis
    6.55 -    by (simp add: convergent_const)
    6.56 -qed
    6.57 +  shows "(\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)) \<Longrightarrow> convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
    6.58 +  by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add)
    6.59  
    6.60  lemma (in bounded_linear) convergent:
    6.61    assumes "convergent (\<lambda>n. X n)"
     7.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Sep 18 17:59:28 2016 +0200
     7.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Sep 18 20:33:48 2016 +0200
     7.3 @@ -34,12 +34,7 @@
     7.4    using add [of x "- y"] by (simp add: minus)
     7.5  
     7.6  lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
     7.7 -  apply (cases "finite A")
     7.8 -   apply (induct set: finite)
     7.9 -    apply (simp add: zero)
    7.10 -   apply (simp add: add)
    7.11 -  apply (simp add: zero)
    7.12 -  done
    7.13 +  by (induct A rule: infinite_finite_induct) (simp_all add: zero add)
    7.14  
    7.15  end
    7.16  
    7.17 @@ -223,10 +218,7 @@
    7.18  
    7.19  lemma setsum_constant_scaleR: "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
    7.20    for y :: "'a::real_vector"
    7.21 -  apply (cases "finite A")
    7.22 -   apply (induct set: finite)
    7.23 -    apply (simp_all add: algebra_simps)
    7.24 -  done
    7.25 +  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
    7.26  
    7.27  lemma vector_add_divide_simps:
    7.28    "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
    7.29 @@ -475,31 +467,17 @@
    7.30    then show thesis ..
    7.31  qed
    7.32  
    7.33 -lemma setsum_in_Reals [intro,simp]:
    7.34 -  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>"
    7.35 -  shows "setsum f s \<in> \<real>"
    7.36 -proof (cases "finite s")
    7.37 -  case True
    7.38 -  then show ?thesis
    7.39 -    using assms by (induct s rule: finite_induct) auto
    7.40 -next
    7.41 -  case False
    7.42 -  then show ?thesis
    7.43 -    using assms by (metis Reals_0 setsum.infinite)
    7.44 -qed
    7.45 +lemma setsum_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setsum f s \<in> \<real>"
    7.46 +proof (induct s rule: infinite_finite_induct)
    7.47 +  case infinite
    7.48 +  then show ?case by (metis Reals_0 setsum.infinite)
    7.49 +qed simp_all
    7.50  
    7.51 -lemma setprod_in_Reals [intro,simp]:
    7.52 -  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>"
    7.53 -  shows "setprod f s \<in> \<real>"
    7.54 -proof (cases "finite s")
    7.55 -  case True
    7.56 -  then show ?thesis
    7.57 -    using assms by (induct s rule: finite_induct) auto
    7.58 -next
    7.59 -  case False
    7.60 -  then show ?thesis
    7.61 -    using assms by (metis Reals_1 setprod.infinite)
    7.62 -qed
    7.63 +lemma setprod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setprod f s \<in> \<real>"
    7.64 +proof (induct s rule: infinite_finite_induct)
    7.65 +  case infinite
    7.66 +  then show ?case by (metis Reals_1 setprod.infinite)
    7.67 +qed simp_all
    7.68  
    7.69  lemma Reals_induct [case_names of_real, induct set: Reals]:
    7.70    "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
    7.71 @@ -1572,16 +1550,8 @@
    7.72  
    7.73  lemma bounded_linear_setsum:
    7.74    fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    7.75 -  assumes "\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)"
    7.76 -  shows "bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
    7.77 -proof (cases "finite I")
    7.78 -  case True
    7.79 -  then show ?thesis
    7.80 -    using assms by induct (auto intro!: bounded_linear_add)
    7.81 -next
    7.82 -  case False
    7.83 -  then show ?thesis by simp
    7.84 -qed
    7.85 +  shows "(\<And>i. i \<in> I \<Longrightarrow> bounded_linear (f i)) \<Longrightarrow> bounded_linear (\<lambda>x. \<Sum>i\<in>I. f i x)"
    7.86 +  by (induct I rule: infinite_finite_induct) (auto intro!: bounded_linear_add)
    7.87  
    7.88  lemma bounded_linear_compose:
    7.89    assumes "bounded_linear f"
     8.1 --- a/src/HOL/Set_Interval.thy	Sun Sep 18 17:59:28 2016 +0200
     8.2 +++ b/src/HOL/Set_Interval.thy	Sun Sep 18 20:33:48 2016 +0200
     8.3 @@ -936,7 +936,7 @@
     8.4    "Suc ` {..<n} = {1..n}"
     8.5    using image_add_atLeastLessThan [of 1 0 n]
     8.6    by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
     8.7 -  
     8.8 +
     8.9  corollary image_Suc_atMost:
    8.10    "Suc ` {..n} = {1..Suc n}"
    8.11    using image_add_atLeastLessThan [of 1 0 "Suc n"]
    8.12 @@ -1198,13 +1198,13 @@
    8.13  lemma subset_eq_atLeast0_lessThan_finite:
    8.14    fixes n :: nat
    8.15    assumes "N \<subseteq> {0..<n}"
    8.16 -  shows "finite N" 
    8.17 +  shows "finite N"
    8.18    using assms finite_atLeastLessThan by (rule finite_subset)
    8.19  
    8.20  lemma subset_eq_atLeast0_atMost_finite:
    8.21    fixes n :: nat
    8.22    assumes "N \<subseteq> {0..n}"
    8.23 -  shows "finite N" 
    8.24 +  shows "finite N"
    8.25    using assms finite_atLeastAtMost by (rule finite_subset)
    8.26  
    8.27  lemma ex_bij_betw_nat_finite:
    8.28 @@ -1992,7 +1992,7 @@
    8.29    proof
    8.30      assume "m \<in> ?A"
    8.31      with assms show "m \<in> ?B"
    8.32 -      by auto 
    8.33 +      by auto
    8.34    next
    8.35      assume "m \<in> ?B"
    8.36      moreover have "m mod n \<in> ?A"
     9.1 --- a/src/HOL/Wellfounded.thy	Sun Sep 18 17:59:28 2016 +0200
     9.2 +++ b/src/HOL/Wellfounded.thy	Sun Sep 18 20:33:48 2016 +0200
     9.3 @@ -790,61 +790,55 @@
     9.4    assumes wf: "wf r"
     9.5    shows "wf (max_ext r)"
     9.6  proof (rule acc_wfI, intro allI)
     9.7 -  fix M
     9.8 -  show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
     9.9 -  proof (cases "finite M")
    9.10 -    case True
    9.11 -    then show ?thesis
    9.12 -    proof (induct M)
    9.13 -      case empty
    9.14 -      show ?case
    9.15 -        by (rule accI) (auto elim: max_ext.cases)
    9.16 -    next
    9.17 -      case (insert a M)
    9.18 -      from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
    9.19 -      proof (induct arbitrary: M)
    9.20 -        fix M a
    9.21 -        assume "M \<in> ?W"
    9.22 -        assume [intro]: "finite M"
    9.23 -        assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
    9.24 -        have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
    9.25 -          if "finite N" "finite M" for N M :: "'a set"
    9.26 -          using that by (induct N arbitrary: M) (auto simp: hyp)
    9.27 -        show "insert a M \<in> ?W"
    9.28 -        proof (rule accI)
    9.29 -          fix N
    9.30 -          assume Nless: "(N, insert a M) \<in> max_ext r"
    9.31 -          then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
    9.32 -            by (auto elim!: max_ext.cases)
    9.33 +  show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M
    9.34 +  proof (induct M rule: infinite_finite_induct)
    9.35 +    case empty
    9.36 +    show ?case
    9.37 +      by (rule accI) (auto elim: max_ext.cases)
    9.38 +  next
    9.39 +    case (insert a M)
    9.40 +    from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
    9.41 +    proof (induct arbitrary: M)
    9.42 +      fix M a
    9.43 +      assume "M \<in> ?W"
    9.44 +      assume [intro]: "finite M"
    9.45 +      assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
    9.46 +      have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
    9.47 +        if "finite N" "finite M" for N M :: "'a set"
    9.48 +        using that by (induct N arbitrary: M) (auto simp: hyp)
    9.49 +      show "insert a M \<in> ?W"
    9.50 +      proof (rule accI)
    9.51 +        fix N
    9.52 +        assume Nless: "(N, insert a M) \<in> max_ext r"
    9.53 +        then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
    9.54 +          by (auto elim!: max_ext.cases)
    9.55  
    9.56 -          let ?N1 = "{n \<in> N. (n, a) \<in> r}"
    9.57 -          let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
    9.58 -          have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
    9.59 -          from Nless have "finite N" by (auto elim: max_ext.cases)
    9.60 -          then have finites: "finite ?N1" "finite ?N2" by auto
    9.61 +        let ?N1 = "{n \<in> N. (n, a) \<in> r}"
    9.62 +        let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
    9.63 +        have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
    9.64 +        from Nless have "finite N" by (auto elim: max_ext.cases)
    9.65 +        then have finites: "finite ?N1" "finite ?N2" by auto
    9.66  
    9.67 -          have "?N2 \<in> ?W"
    9.68 -          proof (cases "M = {}")
    9.69 -            case [simp]: True
    9.70 -            have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
    9.71 -            from * have "?N2 = {}" by auto
    9.72 -            with Mw show "?N2 \<in> ?W" by (simp only:)
    9.73 -          next
    9.74 -            case False
    9.75 -            from * finites have N2: "(?N2, M) \<in> max_ext r"
    9.76 -              by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
    9.77 -            with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
    9.78 -          qed
    9.79 -          with finites have "?N1 \<union> ?N2 \<in> ?W"
    9.80 -            by (rule add_less) simp
    9.81 -          then show "N \<in> ?W" by (simp only: N)
    9.82 +        have "?N2 \<in> ?W"
    9.83 +        proof (cases "M = {}")
    9.84 +          case [simp]: True
    9.85 +          have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
    9.86 +          from * have "?N2 = {}" by auto
    9.87 +          with Mw show "?N2 \<in> ?W" by (simp only:)
    9.88 +        next
    9.89 +          case False
    9.90 +          from * finites have N2: "(?N2, M) \<in> max_ext r"
    9.91 +            by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
    9.92 +          with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
    9.93          qed
    9.94 +        with finites have "?N1 \<union> ?N2 \<in> ?W"
    9.95 +          by (rule add_less) simp
    9.96 +        then show "N \<in> ?W" by (simp only: N)
    9.97        qed
    9.98      qed
    9.99    next
   9.100 -    case [simp]: False
   9.101 -    show ?thesis
   9.102 -      by (rule accI) (auto elim: max_ext.cases)
   9.103 +    case [simp]: infinite
   9.104 +    show ?case by (rule accI) (auto elim: max_ext.cases)
   9.105    qed
   9.106  qed
   9.107