Lemmas about Reals, norm, etc., and cleaner variants of existing ones

--- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 15:45:55 2014 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 16:56:04 2014 +0000
@@ -385,7 +385,7 @@
 apply (erule nonzero_of_real_inverse [symmetric])
 done
 
-lemma Reals_inverse [simp]:
+lemma Reals_inverse:
   fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
   shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
 apply (auto simp add: Reals_def)
@@ -393,6 +393,11 @@
 apply (rule of_real_inverse [symmetric])
 done
 
+lemma Reals_inverse_iff [simp]: 
+  fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
+  shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
+by (metis Reals_inverse inverse_inverse_eq)
+
 lemma nonzero_Reals_divide:
   fixes a b :: "'a::real_field"
   shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
@@ -427,6 +432,24 @@
   then show thesis ..
 qed
 
+lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+proof (cases "finite s")
+  case True then show ?thesis using assms
+    by (induct s rule: finite_induct) auto
+next
+  case False then show ?thesis using assms
+    by (metis Reals_0 setsum_infinite)
+qed
+
+lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+proof (cases "finite s")
+  case True then show ?thesis using assms
+    by (induct s rule: finite_induct) auto
+next
+  case False then show ?thesis using assms
+    by (metis Reals_1 setprod_infinite)
+qed
+
 lemma Reals_induct [case_names of_real, induct set: Reals]:
   "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
   by (rule Reals_cases) auto
@@ -719,6 +742,11 @@
   finally show ?thesis .
 qed
 
+lemma norm_triangle_mono: 
+  fixes a b :: "'a::real_normed_vector"
+  shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
+by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
+
 lemma abs_norm_cancel [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "\<bar>norm a\<bar> = norm a"
@@ -802,6 +830,17 @@
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
+lemma setprod_norm:
+  fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
+  shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
+proof (cases "finite A")
+  case True then show ?thesis 
+    by (induct A rule: finite_induct) (auto simp: norm_mult)
+next
+  case False then show ?thesis
+    by (metis norm_one setprod.infinite) 
+qed
+
 
 subsection {* Metric spaces *}
 

--- a/src/HOL/Set_Interval.thy	Mon Feb 24 15:45:55 2014 +0000
+++ b/src/HOL/Set_Interval.thy	Mon Feb 24 16:56:04 2014 +0000
@@ -1667,7 +1667,13 @@
 
 lemma setprod_power_distrib:
   fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
-  shows "finite A \<Longrightarrow> setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
-  by (induct set: finite) (auto simp: power_mult_distrib)
+  shows "setprod f A ^ n = setprod (\<lambda>x. (f x)^n) A"
+proof (cases "finite A") 
+  case True then show ?thesis 
+    by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
+next
+  case False then show ?thesis 
+    by (metis setprod_infinite power_one)
+qed
 
 end

--- a/src/HOL/Transcendental.thy	Mon Feb 24 15:45:55 2014 +0000
+++ b/src/HOL/Transcendental.thy	Mon Feb 24 16:56:04 2014 +0000
@@ -60,6 +60,23 @@
   apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
   done
 
+lemma power_diff_1_eq:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i=0..<n. (x^i))"
+using lemma_realpow_diff_sumr2 [of x _ 1] 
+  by (cases n) auto
+
+lemma one_diff_power_eq':
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^(n - Suc i))"
+using lemma_realpow_diff_sumr2 [of 1 _ x] 
+  by (cases n) auto
+
+lemma one_diff_power_eq:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^i)"
+by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
+
 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}