# 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 \ (\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 \ B)" + using assms by (auto simp: holomorphic_on_def at_within_open[of _ A] + at_within_open[of _ B] at_within_open[of _ "A \ B"] open_Un) + +lemma holomorphic_on_If_Un [holomorphic_intros]: + assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B" + assumes "\z. z \ A \ z \ B \ f z = g z" + shows "(\z. if z \ A then f z else g z) holomorphic_on (A \ B)" (is "?h holomorphic_on _") +proof (intro holomorphic_on_Un) + note \f holomorphic_on A\ + also have "f holomorphic_on A \ ?h holomorphic_on A" + by (intro holomorphic_cong) auto + finally show \ . +next + note \g holomorphic_on B\ + also have "g holomorphic_on B \ ?h holomorphic_on B" + using assms by (intro holomorphic_cong) auto + finally show \ . +qed (insert assms, auto) + lemma DERIV_deriv_iff_field_differentiable: "DERIV f x :> deriv f x \ 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 "\x. x \ A \ f x abs_summable_on B" + shows "(\y. \x\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 \ (\x. Re (f x)) abs_summable_on A" + by (simp add: abs_summable_on_def) + +lemma abs_summable_Im: "f abs_summable_on A \ (\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 \ B" "finite (B - A)" + shows "f abs_summable_on B" +proof - + have "f abs_summable_on (A \ (B - A))" + by (intro abs_summable_on_union assms abs_summable_on_finite) + also from assms have "A \ (B - A) = B" by blast + finally show ?thesis . +qed + lemma abs_summable_on_reindex_bij_betw: assumes "bij_betw g A B" shows "(\x. f (g x)) abs_summable_on A \ f abs_summable_on B" @@ -407,6 +428,27 @@ lemma infsetsum_all_0: "(\x. x \ A \ f x = 0) \ infsetsum f A = 0" by simp +lemma infsetsum_nonneg: "(\x. x \ A \ f x \ (0::real)) \ infsetsum f A \ 0" + unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto + +lemma sum_infsetsum: + assumes "\x. x \ A \ f x abs_summable_on B" + shows "(\x\A. \\<^sub>ay\B. f x y) = (\\<^sub>ay\B. \x\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 \ Re (infsetsum f A) = (\\<^sub>ax\A. Re (f x))" + by (simp add: infsetsum_def abs_summable_on_def) + +lemma Im_infsetsum: "f abs_summable_on A \ Im (infsetsum f A) = (\\<^sub>ax\A. Im (f x))" + by (simp add: infsetsum_def abs_summable_on_def) + +lemma infsetsum_of_real: + shows "infsetsum (\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 \ infsetsum f A = (\x\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 \ 'a set" for S + where base: "s \ insert 0 S \ s \ group_closure S" +| diff: "s \ group_closure S \ t \ group_closure S \ s - t \ group_closure S" + +lemma zero_in_group_closure [simp]: + "0 \ group_closure S" + using group_closure.base [of 0 S] by simp + +lemma group_closure_minus_iff [simp]: + "- s \ group_closure S \ s \ 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 \ group_closure S" if "s \ group_closure S" and "t \ 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 \ group_closure S" if "s \ 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 \ group_closure S" if "s \ 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]: + "\s\ \ group_closure S \ s \ group_closure S" for s :: int + by (simp add: abs_if) + +lemma group_closure_mult_left: + "s * t \ group_closure S" if "s \ group_closure S" for s t :: int +proof - + from that group_closure_scalar_mult_right [of s S "nat \t\"] + have "s * int (nat \t\) \ group_closure S" + by (simp only:) + then show ?thesis + by (cases "t \ 0") simp_all +qed + +lemma group_closure_mult_right: + "s * t \ group_closure S" if "t \ 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 \ group_closure (times k ` S)" + then show "s \ 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 \ times k ` group_closure S" + then obtain r where r: "r \ group_closure S" and s: "s = k * r" + by auto + from r have "k * r \ group_closure (times k ` S)" + by (induction arbitrary: s) (auto simp add: algebra_simps intro: group_closure.intros) + with s show "s \ 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 \ 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 \ S" for s + proof - + from that have "s \ 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 \ {}" "X \ S" + shows "(\x\X. a x * x) \ 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) \ group_closure S" for S :: "int set" +proof (cases "S \ {0}") + case True + then have "S = {} \ S = {0}" + by auto + then show ?thesis + by auto +next + case False + then obtain s where s: "s \ 0" "s \ S" + by auto + then have s': "\s\ \ 0" "\s\ \ group_closure S" + by (auto intro: group_closure.base) + define m where "m = (LEAST n. n > 0 \ int n \ group_closure S)" + have "m > 0 \ int m \ group_closure S" + unfolding m_def + apply (rule LeastI [of _ "nat \s\"]) + using s' + by simp + then have m: "int m \ 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 \ group_closure S" + show "int m dvd s" + proof (rule ccontr) + assume "\ int m dvd s" + then have *: "0 < s mod int m" + using \0 < m\ le_less by fastforce + have "m \ 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 \ group_closure S" + by (auto intro: group_closure.diff s group_closure_mult_right m) + finally show "int (nat (s mod int m)) \ group_closure S" + by simp + qed + with * have "int m \ s mod int m" + by simp + moreover have "s mod int m < int m" + using \0 < m\ 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 \ 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 \ group_closure S" + then show "s \ 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 \ 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 \ 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]) \ ins_list x (xs @ a # ys) = @@ -105,7 +105,7 @@ done lemma sorted_del_list: "sorted xs \ 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 \ 'b::ord) \ ('a \ bool) \ 'a" where "arg_min f P = (SOME x. is_arg_min f P x)" -abbreviation arg_min_on :: "('a \ 'b::ord) \ 'a set \ 'a" where -"arg_min_on f S \ arg_min f (\x. x \ S)" +definition arg_min_on :: "('a \ 'b::ord) \ 'a set \ 'a" where +"arg_min_on f S = arg_min f (\x. x \ S)" syntax "_arg_min" :: "('a \ 'b) \ pttrn \ bool \ 'a" @@ -908,7 +908,7 @@ lemma arg_min_SOME_Min: "finite S \ arg_min_on f S = (SOME y. y \ S \ 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 \ {}" shows "arg_min_on f S \ S" and "\(\x\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 \ 'b :: linorder" @@ -940,8 +940,8 @@ definition arg_max :: "('a \ 'b::ord) \ ('a \ bool) \ 'a" where "arg_max f P = (SOME x. is_arg_max f P x)" -abbreviation arg_max_on :: "('a \ 'b::ord) \ 'a set \ 'a" where -"arg_max_on f S \ arg_max f (\x. x \ S)" +definition arg_max_on :: "('a \ 'b::ord) \ 'a set \ 'a" where +"arg_max_on f S = arg_max f (\x. x \ S)" syntax "_arg_max" :: "('a \ 'b) \ pttrn \ bool \ '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\Use only if you cannot use @{const Min} instead:\ +fun min_list :: "'a::ord list \ 'a" where +"min_list (x # xs) = (case xs of [] \ x | _ \ min x (min_list xs))" + +text\Returns first minimum:\ +fun arg_min_list :: "('a \ ('b::linorder)) \ 'a list \ '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 \ f m then x else m)" + text\ \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 (\i. i*i) [3,-1,1,-2::int] = -1" by (simp)} \end{tabular}} \caption{Characteristic examples} \label{fig:Characteristic} @@ -793,28 +804,13 @@ "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs" by (fact measure_induct) +lemma induct_list012: + "\P []; \x. P [x]; \x y zs. P (y # zs) \ P (x # y # zs)\ \ P xs" +by induction_schema (pat_completeness, lexicographic_order) + lemma list_nonempty_induct [consumes 1, case_names single cons]: - assumes "xs \ []" - assumes single: "\x. P [x]" - assumes cons: "\x xs. xs \ [] \ P xs \ P (x # xs)" - shows "P xs" -using \xs \ []\ 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 \ []" by simp - with Cons.hyps show "P xs" . - qed - qed -qed + "\ xs \ []; \x. P [x]; \x xs. xs \ [] \ P xs \ P (x # xs)\ \ P xs" +by(induction xs rule: induct_list012) auto lemma inj_split_Cons: "inj_on (\(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 \ [] \ last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)" @@ -2430,11 +2426,7 @@ lemma takeWhile_not_last: "distinct xs \ takeWhile (\y. y \ 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] = [] \ j < i" by (simp add: upto.simps) +lemma upto_Nil2[simp]: "[] = [i..j] \ j < i" +by (simp add: upto.simps) + lemma upto_rec1: "i \ j \ [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 \@{const min} and @{const arg_min}\ + +lemma min_list_Min: "xs \ [] \ min_list xs = Min (set xs)" +by (induction xs rule: induct_list012)(auto) + +lemma f_arg_min_list_f: "xs \ [] \ 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 \ [] \ arg_min_list f xs \ set xs" +by(induction xs rule: induct_list012) (auto simp: Let_def) + subsubsection \(In)finiteness\ @@ -4910,10 +4916,6 @@ subsubsection \@{const sorted_wrt}\ -lemma sorted_wrt_induct: - "\P []; \x. P [x]; \x y zs. P (y # zs) \ P (x # y # zs)\ \ P xs" -by induction_schema (pat_completeness, lexicographic_order) - lemma sorted_wrt_Cons: assumes "transp P" shows "sorted_wrt P (x # xs) = ((\y \ set xs. P x y) \ sorted_wrt P xs)" @@ -4921,7 +4923,7 @@ lemma sorted_wrt_ConsI: "\ \y. y \ set xs \ P x y; sorted_wrt P xs \ \ 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 \ 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 (\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: "(\x y. P x y \ Q x y) \ sorted_wrt P xs \ sorted_wrt Q xs" -by(induction xs rule: sorted_wrt_induct)(auto) +by(induction xs rule: induct_list012)(auto) text \Strictly Ascending Sequences of Natural Numbers\ @@ -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 \ 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 \ '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 \ 'a :: {real_normed_vector,complete_space}" + assumes bound: "eventually (\x0. \a\x0. \b>a. norm (sum f {a<..b}) \ g a) sequentially" + assumes g: "g \ 0" + shows "summable f" unfolding summable_iff_convergent' +proof (intro Cauchy_convergent CauchyI', goal_cases) + case (1 \) + with g have "eventually (\x. \g x\ < \) sequentially" + by (auto simp: tendsto_iff) + from eventually_conj[OF this bound] obtain x0 where x0: + "\x. x \ x0 \ \g x\ < \" "\a b. x0 \ a \ a < b \ norm (sum f {a<..b}) \ g a" + unfolding eventually_at_top_linorder by auto + + show ?case + proof (intro exI[of _ x0] allI impI) + fix m n assume mn: "x0 \ 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}) \ g m" using mn by (intro x0) auto + also have "\ \ \g m\" by simp + also have "\ < \" using mn by (intro x0) auto + finally show "dist (sum f {..m}) (sum f {..n}) < \" . + qed +qed + end