# HG changeset patch
# User wenzelm
# Date 1513247066 -3600
# Node ID 694f29a5433b19128594f9469435dcbe9983792a
# Parent  2f213405cc0eefee5e2b29f7cb223aa39a3690ce# Parent  b335e255ebcc94fd5058f44eb1ed4d0a53059116
merged

diff -r b335e255ebcc -r 694f29a5433b src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -379,6 +379,28 @@
   "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
   by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
 
+lemma holomorphic_on_Un [holomorphic_intros]:
+  assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
+  shows   "f holomorphic_on (A \<union> B)"
+  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
+                             at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
+
+lemma holomorphic_on_If_Un [holomorphic_intros]:
+  assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
+  assumes "\<And>z. z \<in> A \<Longrightarrow> z \<in> B \<Longrightarrow> f z = g z"
+  shows   "(\<lambda>z. if z \<in> A then f z else g z) holomorphic_on (A \<union> B)" (is "?h holomorphic_on _")
+proof (intro holomorphic_on_Un)
+  note \<open>f holomorphic_on A\<close>
+  also have "f holomorphic_on A \<longleftrightarrow> ?h holomorphic_on A"
+    by (intro holomorphic_cong) auto
+  finally show \<dots> .
+next
+  note \<open>g holomorphic_on B\<close>
+  also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
+    using assms by (intro holomorphic_cong) auto
+  finally show \<dots> .
+qed (insert assms, auto)
+
 lemma DERIV_deriv_iff_field_differentiable:
   "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
   unfolding field_differentiable_def by (metis DERIV_imp_deriv)
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -256,6 +256,27 @@
     show "f abs_summable_on insert x A" by simp
 qed
 
+lemma abs_summable_sum: 
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
+  shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
+  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
+
+lemma abs_summable_Re: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Re (f x)) abs_summable_on A"
+  by (simp add: abs_summable_on_def)
+
+lemma abs_summable_Im: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Im (f x)) abs_summable_on A"
+  by (simp add: abs_summable_on_def)
+
+lemma abs_summable_on_finite_diff:
+  assumes "f abs_summable_on A" "A \<subseteq> B" "finite (B - A)"
+  shows   "f abs_summable_on B"
+proof -
+  have "f abs_summable_on (A \<union> (B - A))"
+    by (intro abs_summable_on_union assms abs_summable_on_finite)
+  also from assms have "A \<union> (B - A) = B" by blast
+  finally show ?thesis .
+qed
+
 lemma abs_summable_on_reindex_bij_betw:
   assumes "bij_betw g A B"
   shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
@@ -407,6 +428,27 @@
 lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
   by simp
 
+lemma infsetsum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (0::real)) \<Longrightarrow> infsetsum f A \<ge> 0"
+  unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
+
+lemma sum_infsetsum:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
+  shows   "(\<Sum>x\<in>A. \<Sum>\<^sub>ay\<in>B. f x y) = (\<Sum>\<^sub>ay\<in>B. \<Sum>x\<in>A. f x y)"
+  using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
+
+lemma Re_infsetsum: "f abs_summable_on A \<Longrightarrow> Re (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Re (f x))"
+  by (simp add: infsetsum_def abs_summable_on_def)
+
+lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
+  by (simp add: infsetsum_def abs_summable_on_def)
+
+lemma infsetsum_of_real: 
+  shows "infsetsum (\<lambda>x. of_real (f x) 
+           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
+             of_real (infsetsum f A)"
+  unfolding infsetsum_def
+  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
+
 lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
   by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
 
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Computational_Algebra/Computational_Algebra.thy
--- a/src/HOL/Computational_Algebra/Computational_Algebra.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -8,6 +8,7 @@
   Formal_Power_Series
   Fraction_Field
   Fundamental_Theorem_Algebra
+  Group_Closure
   Normalized_Fraction
   Nth_Powers
   Polynomial_FPS
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -602,6 +602,9 @@
     by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
 qed
 
+lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
+  unfolding One_nat_def [symmetric] using prime_factorization_1 .
+
 instance int :: normalization_euclidean_semiring ..
 
 instance int :: euclidean_ring_gcd
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Computational_Algebra/Group_Closure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/Group_Closure.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -0,0 +1,210 @@
+(*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
+    Author:     Johannes Hoelzl, TU Muenchen
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+theory Group_Closure
+imports
+  Main
+begin
+
+context ab_group_add
+begin
+
+inductive_set group_closure :: "'a set \<Rightarrow> 'a set" for S
+  where base: "s \<in> insert 0 S \<Longrightarrow> s \<in> group_closure S"
+| diff: "s \<in> group_closure S \<Longrightarrow> t \<in> group_closure S \<Longrightarrow> s - t \<in> group_closure S"
+
+lemma zero_in_group_closure [simp]:
+  "0 \<in> group_closure S"
+  using group_closure.base [of 0 S] by simp
+
+lemma group_closure_minus_iff [simp]:
+  "- s \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S"
+  using group_closure.diff [of 0 S s] group_closure.diff [of 0 S "- s"] by auto
+
+lemma group_closure_add:
+  "s + t \<in> group_closure S" if "s \<in> group_closure S" and "t \<in> group_closure S"
+  using that group_closure.diff [of s S "- t"] by auto
+
+lemma group_closure_empty [simp]:
+  "group_closure {} = {0}"
+  by (rule ccontr) (auto elim: group_closure.induct)
+
+lemma group_closure_insert_zero [simp]:
+  "group_closure (insert 0 S) = group_closure S"
+  by (auto elim: group_closure.induct intro: group_closure.intros)
+
+end
+
+context comm_ring_1
+begin
+
+lemma group_closure_scalar_mult_left:
+  "of_nat n * s \<in> group_closure S" if "s \<in> group_closure S"
+  using that by (induction n) (auto simp add: algebra_simps intro: group_closure_add)
+
+lemma group_closure_scalar_mult_right:
+  "s * of_nat n \<in> group_closure S" if "s \<in> group_closure S"
+  using that group_closure_scalar_mult_left [of s S n] by (simp add: ac_simps)
+
+end
+
+lemma group_closure_abs_iff [simp]:
+  "\<bar>s\<bar> \<in> group_closure S \<longleftrightarrow> s \<in> group_closure S" for s :: int
+  by (simp add: abs_if)
+
+lemma group_closure_mult_left:
+  "s * t \<in> group_closure S" if "s \<in> group_closure S" for s t :: int
+proof -
+  from that group_closure_scalar_mult_right [of s S "nat \<bar>t\<bar>"]
+    have "s * int (nat \<bar>t\<bar>) \<in> group_closure S"
+    by (simp only:)
+  then show ?thesis
+    by (cases "t \<ge> 0") simp_all
+qed
+
+lemma group_closure_mult_right:
+  "s * t \<in> group_closure S" if "t \<in> group_closure S" for s t :: int
+  using that group_closure_mult_left [of t S s] by (simp add: ac_simps)
+
+context idom
+begin
+
+lemma group_closure_mult_all_eq:
+  "group_closure (times k ` S) = times k ` group_closure S"
+proof (rule; rule)
+  fix s
+  have *: "k * a + k * b = k * (a + b)"
+    "k * a - k * b = k * (a - b)" for a b
+    by (simp_all add: algebra_simps)
+  assume "s \<in> group_closure (times k ` S)"
+  then show "s \<in> times k ` group_closure S"
+    by induction (auto simp add: * image_iff intro: group_closure.base group_closure.diff bexI [of _ 0])
+next
+  fix s
+  assume "s \<in> times k ` group_closure S"
+  then obtain r where r: "r \<in> group_closure S" and s: "s = k * r"
+    by auto
+  from r have "k * r \<in> group_closure (times k ` S)"
+    by (induction arbitrary: s) (auto simp add: algebra_simps intro: group_closure.intros)
+  with s show "s \<in> group_closure (times k ` S)"
+    by simp
+qed
+
+end
+
+lemma Gcd_group_closure_eq_Gcd:
+  "Gcd (group_closure S) = Gcd S" for S :: "int set"
+proof (rule associated_eqI)
+  have "Gcd S dvd s" if "s \<in> group_closure S" for s
+    using that by induction auto
+  then show "Gcd S dvd Gcd (group_closure S)"
+    by auto
+  have "Gcd (group_closure S) dvd s" if "s \<in> S" for s
+  proof -
+    from that have "s \<in> group_closure S"
+      by (simp add: group_closure.base)
+    then show ?thesis
+      by (rule Gcd_dvd)
+  qed
+  then show "Gcd (group_closure S) dvd Gcd S"
+    by auto
+qed simp_all
+
+lemma group_closure_sum:
+  fixes S :: "int set"
+  assumes X: "finite X" "X \<noteq> {}" "X \<subseteq> S"
+  shows "(\<Sum>x\<in>X. a x * x) \<in> group_closure S"
+  using X by (induction X rule: finite_ne_induct)
+    (auto intro: group_closure_mult_right group_closure.base group_closure_add)
+
+lemma Gcd_group_closure_in_group_closure:
+  "Gcd (group_closure S) \<in> group_closure S" for S :: "int set"
+proof (cases "S \<subseteq> {0}")
+  case True
+  then have "S = {} \<or> S = {0}"
+    by auto
+  then show ?thesis
+    by auto
+next
+  case False
+  then obtain s where s: "s \<noteq> 0" "s \<in> S"
+    by auto
+  then have s': "\<bar>s\<bar> \<noteq> 0" "\<bar>s\<bar> \<in> group_closure S"
+    by (auto intro: group_closure.base)
+  define m where "m = (LEAST n. n > 0 \<and> int n \<in> group_closure S)"
+  have "m > 0 \<and> int m \<in> group_closure S"
+    unfolding m_def
+    apply (rule LeastI [of _ "nat \<bar>s\<bar>"])
+    using s'
+    by simp
+  then have m: "int m \<in> group_closure S" and "0 < m"
+    by auto
+
+  have "Gcd (group_closure S) = int m"
+  proof (rule associated_eqI)
+    from m show "Gcd (group_closure S) dvd int m"
+      by (rule Gcd_dvd)
+    show "int m dvd Gcd (group_closure S)"
+    proof (rule Gcd_greatest)
+      fix s
+      assume s: "s \<in> group_closure S"
+      show "int m dvd s"
+      proof (rule ccontr)
+        assume "\<not> int m dvd s"
+        then have *: "0 < s mod int m"
+          using \<open>0 < m\<close> le_less by fastforce
+        have "m \<le> nat (s mod int m)"
+        proof (subst m_def, rule Least_le, rule)
+          from * show "0 < nat (s mod int m)"
+            by simp
+          from minus_div_mult_eq_mod [symmetric, of s "int m"]
+          have "s mod int m = s - s div int m * int m"
+            by auto
+          also have "s - s div int m * int m \<in> group_closure S"
+            by (auto intro: group_closure.diff s group_closure_mult_right m)
+          finally  show "int (nat (s mod int m)) \<in> group_closure S"
+            by simp
+        qed
+        with * have "int m \<le> s mod int m"
+          by simp
+        moreover have "s mod int m < int m"
+          using \<open>0 < m\<close> by simp
+        ultimately show False
+          by auto
+      qed
+    qed
+  qed simp_all
+  with m show ?thesis
+    by simp
+qed
+
+lemma Gcd_in_group_closure:
+  "Gcd S \<in> group_closure S" for S :: "int set"
+  using Gcd_group_closure_in_group_closure [of S]
+  by (simp add: Gcd_group_closure_eq_Gcd)
+
+lemma group_closure_eq:
+  "group_closure S = range (times (Gcd S))" for S :: "int set"
+proof (auto intro: Gcd_in_group_closure group_closure_mult_left)
+  fix s
+  assume "s \<in> group_closure S"
+  then show "s \<in> range (times (Gcd S))"
+  proof induction
+    case (base s)
+    then have "Gcd S dvd s"
+      by (auto intro: Gcd_dvd)
+    then obtain t where "s = Gcd S * t" ..
+    then show ?case
+      by auto
+  next
+    case (diff s t)
+    moreover have "Gcd S * a - Gcd S * b = Gcd S * (a - b)" for a b
+      by (simp add: algebra_simps)
+    ultimately show ?case
+      by auto
+  qed
+qed
+
+end
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Data_Structures/List_Ins_Del.thy
--- a/src/HOL/Data_Structures/List_Ins_Del.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -53,12 +53,12 @@
 by(induction xs) auto
 
 lemma distinct_if_sorted: "sorted xs \<Longrightarrow> distinct xs"
-apply(induction xs rule: sorted_wrt_induct)
+apply(induction xs rule: induct_list012)
 apply auto
 by (metis in_set_conv_decomp_first less_imp_not_less sorted_mid_iff2)
 
 lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)"
-by(induction xs rule: sorted_wrt_induct) auto
+by(induction xs rule: induct_list012) auto
 
 lemma ins_list_sorted: "sorted (xs @ [a]) \<Longrightarrow>
   ins_list x (xs @ a # ys) =
@@ -105,7 +105,7 @@
 done
 
 lemma sorted_del_list: "sorted xs \<Longrightarrow> sorted(del_list x xs)"
-apply(induction xs rule: sorted_wrt_induct)
+apply(induction xs rule: induct_list012)
 apply auto
 by (meson order.strict_trans sorted_Cons_iff)
 
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Lattices_Big.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -832,8 +832,8 @@
 definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
 "arg_min f P = (SOME x. is_arg_min f P x)"
 
-abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
-"arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)"
+definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)"
 
 syntax
   "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
@@ -908,7 +908,7 @@
 
 lemma arg_min_SOME_Min:
   "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
-unfolding arg_min_def is_arg_min_linorder
+unfolding arg_min_on_def arg_min_def is_arg_min_linorder
 apply(rule arg_cong[where f = Eps])
 apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
 done
@@ -917,7 +917,7 @@
 assumes "finite S" "S \<noteq> {}"
 shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
 using ex_is_arg_min_if_finite[OF assms, of f]
-unfolding arg_min_def is_arg_min_def
+unfolding arg_min_on_def arg_min_def is_arg_min_def
 by(auto dest!: someI_ex)
 
 lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
@@ -940,8 +940,8 @@
 definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
 "arg_max f P = (SOME x. is_arg_max f P x)"
 
-abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
-"arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)"
+definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
+"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)"
 
 syntax
   "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
diff -r b335e255ebcc -r 694f29a5433b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/List.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -270,6 +270,15 @@
   by pat_completeness simp_all
 termination by lexicographic_order
 
+text\<open>Use only if you cannot use @{const Min} instead:\<close>
+fun min_list :: "'a::ord list \<Rightarrow> 'a" where
+"min_list (x # xs) = (case xs of [] \<Rightarrow> x | _ \<Rightarrow> min x (min_list xs))"
+
+text\<open>Returns first minimum:\<close>
+fun arg_min_list :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> 'a" where
+"arg_min_list f [x] = x" |
+"arg_min_list f (x#y#zs) = (let m = arg_min_list f (y#zs) in if f x \<le> f m then x else m)"
+
 text\<open>
 \begin{figure}[htbp]
 \fbox{
@@ -324,7 +333,9 @@
 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
-@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}
+@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
+@{lemma "min_list [3,1,-2::int] = -2" by (simp)}\\
+@{lemma "arg_min_list (\<lambda>i. i*i) [3,-1,1,-2::int] = -1" by (simp)}
 \end{tabular}}
 \caption{Characteristic examples}
 \label{fig:Characteristic}
@@ -793,28 +804,13 @@
   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
 by (fact measure_induct)
 
+lemma induct_list012:
+  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
+by induction_schema (pat_completeness, lexicographic_order)
+
 lemma list_nonempty_induct [consumes 1, case_names single cons]:
-  assumes "xs \<noteq> []"
-  assumes single: "\<And>x. P [x]"
-  assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
-  shows "P xs"
-using \<open>xs \<noteq> []\<close> proof (induct xs)
-  case Nil then show ?case by simp
-next
-  case (Cons x xs)
-  show ?case
-  proof (cases xs)
-    case Nil
-    with single show ?thesis by simp
-  next
-    case Cons
-    show ?thesis
-    proof (rule cons)
-      from Cons show "xs \<noteq> []" by simp
-      with Cons.hyps show "P xs" .
-    qed
-  qed
-qed
+  "\<lbrakk> xs \<noteq> []; \<And>x. P [x]; \<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)\<rbrakk> \<Longrightarrow> P xs"
+by(induction xs rule: induct_list012) auto
 
 lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
   by (auto intro!: inj_onI)
@@ -1986,7 +1982,7 @@
 by(induct xs)(auto simp:neq_Nil_conv)
 
 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
-by (induct xs, simp, case_tac xs, simp_all)
+by (induction xs rule: induct_list012) simp_all
 
 lemma last_list_update:
   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
@@ -2430,11 +2426,7 @@
 
 lemma takeWhile_not_last:
   "distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
-apply(induct xs)
- apply simp
-apply(case_tac xs)
-apply(auto)
-done
+by(induction xs rule: induct_list012) auto
 
 lemma takeWhile_cong [fundef_cong]:
   "[| l = k; !!x. x : set l ==> P x = Q x |]
@@ -3229,6 +3221,9 @@
 lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
 by (simp add: upto.simps)
 
+lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i"
+by (simp add: upto.simps)
+
 lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
 by(simp add: upto.simps)
 
@@ -4811,6 +4806,17 @@
     by (simp add: nth_transpose filter_map comp_def)
 qed
 
+subsubsection \<open>@{const min} and @{const arg_min}\<close>
+
+lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
+by (induction xs rule: induct_list012)(auto)
+
+lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
+by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
+
+lemma arg_min_list_in: "xs \<noteq> [] \<Longrightarrow> arg_min_list f xs \<in> set xs"
+by(induction xs rule: induct_list012) (auto simp: Let_def)
+
 
 subsubsection \<open>(In)finiteness\<close>
 
@@ -4910,10 +4916,6 @@
 
 subsubsection \<open>@{const sorted_wrt}\<close>
 
-lemma sorted_wrt_induct:
-  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
-by induction_schema (pat_completeness, lexicographic_order)
-
 lemma sorted_wrt_Cons:
 assumes "transp P"
 shows   "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
@@ -4921,7 +4923,7 @@
 
 lemma sorted_wrt_ConsI:
   "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
-by (induction xs rule: sorted_wrt_induct) simp_all
+by (induction xs rule: induct_list012) simp_all
 
 lemma sorted_wrt_append:
 assumes "transp P"
@@ -4931,15 +4933,15 @@
 
 lemma sorted_wrt_backwards:
   "sorted_wrt P (xs @ [y, z]) = (P y z \<and> sorted_wrt P (xs @ [y]))"
-by (induction xs rule: sorted_wrt_induct) auto
+by (induction xs rule: induct_list012) auto
 
 lemma sorted_wrt_rev:
   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
-by (induction xs rule: sorted_wrt_induct) (simp_all add: sorted_wrt_backwards)
+by (induction xs rule: induct_list012) (simp_all add: sorted_wrt_backwards)
 
 lemma sorted_wrt_mono:
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
-by(induction xs rule: sorted_wrt_induct)(auto)
+by(induction xs rule: induct_list012)(auto)
 
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
@@ -4976,7 +4978,7 @@
   proof (induct xs rule: sorted.induct)
     case (Cons xs x) thus ?case by (cases xs) simp_all
   qed simp
-qed (induct xs rule: sorted_wrt_induct, simp_all)
+qed (induct xs rule: induct_list012, simp_all)
 
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Number_Theory/Prime_Powers.thy
--- a/src/HOL/Number_Theory/Prime_Powers.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -422,7 +422,13 @@
 
 definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
   "mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
-  
+
+lemma mangoldt_0 [simp]: "mangoldt 0 = 0"
+  by (simp add: mangoldt_def)
+
+lemma mangoldt_Suc_0 [simp]: "mangoldt (Suc 0) = 0"
+  by (simp add: mangoldt_def)
+
 lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n"
   by (simp add: mangoldt_def)
 
@@ -481,6 +487,10 @@
   with True show ?thesis by (auto simp: mangoldt_def abs_if)
 qed (auto simp: mangoldt_def)
 
+lemma Re_mangoldt [simp]: "Re (mangoldt n) = mangoldt n"
+  and Im_mangoldt [simp]: "Im (mangoldt n) = 0"
+  by (simp_all add: mangoldt_def)
+
 lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
   using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .
 
diff -r b335e255ebcc -r 694f29a5433b src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Dec 13 18:01:22 2017 +0100
+++ b/src/HOL/Series.thy	Thu Dec 14 11:24:26 2017 +0100
@@ -1223,4 +1223,32 @@
   ultimately show ?thesis by simp
 qed
 
+lemma summable_bounded_partials:
+  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_vector,complete_space}"
+  assumes bound: "eventually (\<lambda>x0. \<forall>a\<ge>x0. \<forall>b>a. norm (sum f {a<..b}) \<le> g a) sequentially"
+  assumes g: "g \<longlonglongrightarrow> 0"
+  shows   "summable f" unfolding summable_iff_convergent'
+proof (intro Cauchy_convergent CauchyI', goal_cases)
+  case (1 \<epsilon>)
+  with g have "eventually (\<lambda>x. \<bar>g x\<bar> < \<epsilon>) sequentially"
+    by (auto simp: tendsto_iff)
+  from eventually_conj[OF this bound] obtain x0 where x0:
+    "\<And>x. x \<ge> x0 \<Longrightarrow> \<bar>g x\<bar> < \<epsilon>" "\<And>a b. x0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> norm (sum f {a<..b}) \<le> g a" 
+    unfolding eventually_at_top_linorder by auto
+
+  show ?case
+  proof (intro exI[of _ x0] allI impI)
+    fix m n assume mn: "x0 \<le> m" "m < n"
+    have "dist (sum f {..m}) (sum f {..n}) = norm (sum f {..n} - sum f {..m})"
+      by (simp add: dist_norm norm_minus_commute)
+    also have "sum f {..n} - sum f {..m} = sum f ({..n} - {..m})"
+      using mn by (intro Groups_Big.sum_diff [symmetric]) auto
+    also have "{..n} - {..m} = {m<..n}" using mn by auto
+    also have "norm (sum f {m<..n}) \<le> g m" using mn by (intro x0) auto
+    also have "\<dots> \<le> \<bar>g m\<bar>" by simp
+    also have "\<dots> < \<epsilon>" using mn by (intro x0) auto
+    finally show "dist (sum f {..m}) (sum f {..n}) < \<epsilon>" .
+  qed
+qed
+
 end