--- 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)
--- 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)
--- 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
--- 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
--- /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
--- 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)
--- 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"
--- 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)"
--- 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] .
--- 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