# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1513976407 0
# Node ID bdf25939a5508d44d8ec9b1aecf4cbee20433f42
# Parent  6c837185aa61d0bf8ce75fd6282009928a5d0310
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -1851,9 +1851,35 @@
 using field_differentiable_def has_field_derivative_powr_right by blast
 
 lemma holomorphic_on_powr_right [holomorphic_intros]:
-    "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
-  unfolding holomorphic_on_def field_differentiable_def
-  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+  assumes "f holomorphic_on s"
+  shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
+proof (cases "w = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  with assms show ?thesis
+    unfolding holomorphic_on_def field_differentiable_def
+    by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+qed
+
+lemma holomorphic_on_divide_gen [holomorphic_intros]:
+  assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
+shows "(\<lambda>z. f z / g z) holomorphic_on s"
+proof (cases "\<exists>z\<in>s. g z = 0")
+  case True
+  with 0 have "g z = 0" if "z \<in> s" for z
+    using that by blast
+  then show ?thesis
+    using g holomorphic_transform by auto
+next
+  case False
+  with 0 have "g z \<noteq> 0" if "z \<in> s" for z
+    using that by blast
+  with holomorphic_on_divide show ?thesis
+    using f g by blast
+qed
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Analysis/Infinite_Set_Sum.thy
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -175,6 +175,9 @@
 lemma abs_summable_on_normI: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
   by simp
 
+lemma abs_summable_complex_of_real [simp]: "(\<lambda>n. complex_of_real (f n)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
+  by (simp add: abs_summable_on_def complex_of_real_integrable_eq)
+
 lemma abs_summable_on_comparison_test:
   assumes "g abs_summable_on A"
   assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
@@ -227,6 +230,23 @@
   "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
   by (subst abs_summable_on_nat_iff) auto
 
+lemma nat_abs_summable_on_comparison_test:
+  fixes f :: "nat \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes "g abs_summable_on I"
+  assumes "\<And>n. \<lbrakk>n\<ge>N; n \<in> I\<rbrakk> \<Longrightarrow> norm (f n) \<le> g n"
+  shows   "f abs_summable_on I"
+  using assms by (fastforce simp add: abs_summable_on_nat_iff intro: summable_comparison_test')
+
+lemma abs_summable_comparison_test_ev:
+  assumes "g abs_summable_on I"
+  assumes "eventually (\<lambda>x. x \<in> I \<longrightarrow> norm (f x) \<le> g x) sequentially"
+  shows   "f abs_summable_on I"
+  by (metis (no_types, lifting) nat_abs_summable_on_comparison_test eventually_at_top_linorder assms)
+
+lemma abs_summable_on_Cauchy:
+  "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. (\<Sum>x = m..<n. norm (f x)) < e)"
+  by (simp add: abs_summable_on_nat_iff' summable_Cauchy sum_nonneg)
+
 lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
   unfolding abs_summable_on_def by (rule integrable_count_space)
 
diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Groups_Big.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -495,12 +495,12 @@
 
 end
 
-text \<open>Now: lot's of fancy syntax. First, @{term "sum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
+text \<open>Now: lots of fancy syntax. First, @{term "sum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
 
 syntax (ASCII)
-  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
+  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM (_/:_)./ _)" [0, 51, 10] 10)
 syntax
-  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
+  "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A"
 
@@ -1062,9 +1062,9 @@
 end
 
 syntax (ASCII)
-  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD (_/:_)./ _)" [0, 51, 10] 10)
 syntax
-  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
 
diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Series.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -564,6 +564,9 @@
 lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
 
+lemma summable_inverse_divide: "summable (inverse \<circ> f) \<Longrightarrow> summable (\<lambda>n. c / f n)"
+  by (auto dest: summable_mult [of _ c] simp: field_simps)
+
 lemma sums_mult_D: "(\<lambda>n. c * f n) sums a \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> f sums (a/c)"
   using sums_mult_iff by fastforce
 
@@ -657,31 +660,52 @@
 
 text \<open>Cauchy-type criterion for convergence of series (c.f. Harrison).\<close>
 
-lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e)"
+lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e)" (is "_ = ?rhs")
   for f :: "nat \<Rightarrow> 'a::banach"
-  apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
-  apply safe
-   apply (drule spec)
-   apply (drule (1) mp)
-   apply (erule exE)
-   apply (rule_tac x="M" in exI)
-   apply clarify
-   apply (rule_tac x="m" and y="n" in linorder_le_cases)
-    apply (frule (1) order_trans)
-    apply (drule_tac x="n" in spec)
-    apply (drule (1) mp)
-    apply (drule_tac x="m" in spec)
-    apply (drule (1) mp)
-    apply (simp_all add: sum_diff [symmetric])
-  apply (drule spec)
-  apply (drule (1) mp)
-  apply (erule exE)
-  apply (rule_tac x="N" in exI)
-  apply clarify
-  apply (rule_tac x="m" and y="n" in linorder_le_cases)
-   apply (subst norm_minus_commute)
-   apply (simp_all add: sum_diff [symmetric])
-  done
+proof
+  assume f: "summable f"
+  show ?rhs
+  proof clarify
+    fix e :: real
+    assume "0 < e"
+    then obtain M where M: "\<And>m n. \<lbrakk>m\<ge>M; n\<ge>M\<rbrakk> \<Longrightarrow> norm (sum f {..<m} - sum f {..<n}) < e"
+      using f by (force simp add: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
+    have "norm (sum f {m..<n}) < e" if "m \<ge> M" for m n
+    proof (cases m n rule: linorder_class.le_cases)
+      assume "m \<le> n"
+      then show ?thesis
+        by (metis (mono_tags, hide_lams) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
+    next
+      assume "n \<le> m"
+      then show ?thesis
+        by (simp add: \<open>0 < e\<close>)
+    qed
+    then show "\<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e"
+      by blast
+  qed
+next
+  assume r: ?rhs
+  then show "summable f"
+    unfolding summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff
+  proof clarify
+    fix e :: real
+    assume "0 < e"
+    with r obtain N where N: "\<And>m n. m \<ge> N \<Longrightarrow> norm (sum f {m..<n}) < e"
+      by blast
+    have "norm (sum f {..<m} - sum f {..<n}) < e" if "m\<ge>N" "n\<ge>N" for m n
+    proof (cases m n rule: linorder_class.le_cases)
+      assume "m \<le> n"
+      then show ?thesis
+        by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute \<open>m\<ge>N\<close>)
+    next
+      assume "n \<le> m"
+      then show ?thesis
+        by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff \<open>n\<ge>N\<close>)
+    qed
+    then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (sum f {..<m} - sum f {..<n}) < e"
+      by blast
+  qed
+qed
 
 context
   fixes f :: "nat \<Rightarrow> 'a::banach"
@@ -708,23 +732,32 @@
 
 text \<open>Comparison tests.\<close>
 
-lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
-  apply (simp add: summable_Cauchy)
-  apply safe
-  apply (drule_tac x="e" in spec)
-  apply safe
-  apply (rule_tac x = "N + Na" in exI)
-  apply safe
-  apply (rotate_tac 2)
-  apply (drule_tac x = m in spec)
-  apply auto
-  apply (rotate_tac 2)
-  apply (drule_tac x = n in spec)
-  apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
-   apply (rule norm_sum)
-  apply (rule_tac y = "sum g {m..<n}" in order_le_less_trans)
-   apply (auto intro: sum_mono simp add: abs_less_iff)
-  done
+lemma summable_comparison_test: 
+  assumes fg: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n" and g: "summable g"
+  shows "summable f"
+proof -
+  obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> norm (f n) \<le> g n" 
+    using assms by blast
+  show ?thesis
+  proof (clarsimp simp add: summable_Cauchy)
+    fix e :: real
+    assume "0 < e"
+    then obtain Ng where Ng: "\<And>m n. m \<ge> Ng \<Longrightarrow> norm (sum g {m..<n}) < e" 
+      using g by (fastforce simp: summable_Cauchy)
+    with N have "norm (sum f {m..<n}) < e" if "m\<ge>max N Ng" for m n
+    proof -
+      have "norm (sum f {m..<n}) \<le> sum g {m..<n}"
+        using N that by (force intro: sum_norm_le)
+      also have "... \<le> norm (sum g {m..<n})"
+        by simp
+      also have "... < e"
+        using Ng that by auto
+      finally show ?thesis .
+    qed
+    then show "\<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e" 
+      by blast
+  qed
+qed
 
 lemma summable_comparison_test_ev:
   "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Set.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -44,9 +44,9 @@
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
 syntax (ASCII)
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ :/ _./ _})")
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/: _)./ _})")
 syntax
-  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ \<in>/ _./ _})")
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/\<in> _)./ _})")
 translations
   "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
@@ -187,21 +187,21 @@
   where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> "bounded existential quantifiers"
 
 syntax (ASCII)
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
-  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST _:_./ _)" [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3ALL (_/:_)./ _)" [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX (_/:_)./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3EX! (_/:_)./ _)" [0, 0, 10] 10)
+  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST (_/:_)./ _)" [0, 0, 10] 10)
 
 syntax (input)
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3! (_/:_)./ _)" [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3? (_/:_)./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3?! (_/:_)./ _)" [0, 0, 10] 10)
 
 syntax
-  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
-  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
-  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
+  "_Ball"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/\<in>_)./ _)" [0, 0, 10] 10)
+  "_Bex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/\<in>_)./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
+  "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
 
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
diff -r 6c837185aa61 -r bdf25939a550 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Transcendental.thy	Fri Dec 22 21:00:07 2017 +0000
@@ -2522,7 +2522,7 @@
   by (simp add: powr_def exp_minus [symmetric])
 
 lemma powr_minus_divide: "x powr (- a) = 1/(x powr a)"
-  for x a :: real
+      for a x :: "'a::{ln,real_normed_field}"
   by (simp add: divide_inverse powr_minus)
 
 lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"