# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1425576629 0
# Node ID 7103019278f03c7fbf6ec9c1dd786e7c7d4dfb90
# Parent  304ee0a475d193f3d68ff14192fbabe3111bf116
The function frac. Various lemmas about limits, series, the exp function, etc.

diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -150,6 +150,11 @@
 lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
+lemma floor_unique_iff:
+  fixes x :: "'a::floor_ceiling"
+  shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
+using floor_correct floor_unique by auto
+
 lemma of_int_floor_le: "of_int (floor x) \<le> x"
   using floor_correct ..
 
@@ -281,6 +286,9 @@
 lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
   using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
 
+lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
+  by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
+
 lemma floor_diff_numeral [simp]:
   "floor (x - numeral v) = floor x - numeral v"
   using floor_diff_of_int [of x "numeral v"] by simp
@@ -464,4 +472,65 @@
 lemma ceiling_minus: "ceiling (- x) = - floor x"
   unfolding ceiling_def by simp
 
+subsection {* Frac Function *}
+
+
+definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
+  "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
+
+lemma frac_lt_1: "frac x < 1"
+  by  (simp add: frac_def) linarith
+
+lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
+  by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
+
+lemma frac_ge_0 [simp]: "frac x \<ge> 0"
+  unfolding frac_def
+  by linarith
+
+lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
+  by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
+
+lemma frac_of_int [simp]: "frac (of_int z) = 0"
+  by (simp add: frac_def)
+
+lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"  
+proof -
+  {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
+   then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
+     by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
+   }
+  moreover
+  { assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
+    then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
+      apply (simp add: floor_unique_iff)
+      apply (auto simp add: algebra_simps)
+      by linarith    
+  }
+  ultimately show ?thesis
+    by (auto simp add: frac_def algebra_simps)
+qed
+
+lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
+                                 else (frac x + frac y) - 1)"  
+  by (simp add: frac_def floor_add)
+
+lemma frac_unique_iff:
+  fixes x :: "'a::floor_ceiling"
+  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
+  apply (auto simp: Ints_def frac_def)
+  apply linarith
+  apply linarith
+  by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
+
+lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
+  by (simp add: frac_unique_iff)
+  
+lemma frac_neg:
+  fixes x :: "'a::floor_ceiling"
+  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
+  apply (auto simp add: frac_unique_iff)
+  apply (simp add: frac_def)
+  by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
+
 end
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Complex.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -73,7 +73,7 @@
 definition "x / (y\<Colon>complex) = x * inverse y"
 
 instance
-  by intro_classes 
+  by intro_classes
      (simp_all add: complex_eq_iff divide_complex_def
       distrib_left distrib_right right_diff_distrib left_diff_distrib
       power2_eq_square add_divide_distrib [symmetric])
@@ -161,6 +161,12 @@
 lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
   by (simp add: of_real_def)
 
+lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"
+  by (simp add: Re_divide sqr_conv_mult)
+
+lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
+  by (simp add: Im_divide sqr_conv_mult)
+
 subsection {* The Complex Number $i$ *}
 
 primcorec "ii" :: complex  ("\<i>") where
@@ -206,6 +212,9 @@
 lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
   by (simp add: complex_eq_iff polar_Ex)
 
+lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
+  by (metis mult.commute power2_i power_mult)
+
 subsection {* Vector Norm *}
 
 instantiation complex :: real_normed_field
@@ -501,11 +510,11 @@
 
 lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
   by (auto simp add: Re_divide)
-  
+
 lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
   by (auto simp add: Im_divide)
 
-lemma complex_div_gt_0: 
+lemma complex_div_gt_0:
   "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
 proof cases
   assume "b = 0" then show ?thesis by auto
@@ -547,7 +556,7 @@
 
 lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
   unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
-  
+
 lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
   unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)
 
@@ -841,7 +850,7 @@
     by auto
 qed
 
-lemma csqrt_minus [simp]: 
+lemma csqrt_minus [simp]:
   assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
   shows "csqrt (- x) = \<i> * csqrt x"
 proof -
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Int.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -498,8 +498,16 @@
 text{*Now we replace the case analysis rule by a more conventional one:
 whether an integer is negative or not.*}
 
+text{*This version is symmetric in the two subgoals.*}
+theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
+  "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+apply (cases "z < 0")
+apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
+done
+
+text{*This is the default, with a negative case.*}
 theorem int_cases [case_names nonneg neg, cases type: int]:
-  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
+  "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
 apply (cases "z < 0")
 apply (blast dest!: negD)
 apply (simp add: linorder_not_less del: of_nat_Suc)
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Limits.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -42,6 +42,11 @@
   shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
   by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
 
+lemma lim_infinity_imp_sequentially:
+  "(f ---> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) ---> l) sequentially"
+by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
+
+
 subsubsection {* Boundedness *}
 
 definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
@@ -885,7 +890,6 @@
   qed
 qed force
 
-
 subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
 
 text {*
@@ -1093,6 +1097,36 @@
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
 
+
+lemma at_to_infinity:
+  fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
+  shows "(at (0::'a)) = filtermap inverse at_infinity"
+proof (rule antisym)
+  have "(inverse ---> (0::'a)) at_infinity"
+    by (fact tendsto_inverse_0)
+  then show "filtermap inverse at_infinity \<le> at (0::'a)"
+    apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def)
+    apply (rule_tac x="1" in exI, auto)
+    done
+next
+  have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity"
+    using filterlim_inverse_at_infinity unfolding filterlim_def
+    by (rule filtermap_mono)
+  then show "at (0::'a) \<le> filtermap inverse at_infinity"
+    by (simp add: filtermap_ident filtermap_filtermap)
+qed
+
+lemma lim_at_infinity_0:
+  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
+  shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
+by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
+
+lemma lim_zero_infinity:
+  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
+  shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
+by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
+
+
 text {*
 
 We only show rules for multiplication and addition when the functions are either against a real
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -853,6 +853,12 @@
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
+text{*Despite a superficial resemblance, @{text norm_eq_1} is not relevant.*}
+lemma square_norm_one:
+  fixes x :: "'a::real_normed_div_algebra"
+  assumes "x^2 = 1" shows "norm x = 1"
+  by (metis assms norm_minus_cancel norm_one power2_eq_1_iff)
+
 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)"
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Series.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -125,6 +125,11 @@
 lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
   by (metis summable_sums sums_summable sums_unique)
 
+lemma sums_unique2:
+  fixes a b :: "'a::{comm_monoid_add,t2_space}"
+  shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
+by (simp add: sums_iff)
+
 lemma suminf_finite:
   assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   shows "suminf f = (\<Sum>n\<in>N. f n)"
@@ -316,6 +321,12 @@
 
 end
 
+lemma summable_minus_iff:
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
+  by (auto dest: summable_minus) --{*used two ways, hence must be outside the context above*}
+
+
 context
   fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
 begin
diff -r 304ee0a475d1 -r 7103019278f0 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 05 11:11:42 2015 +0100
+++ b/src/HOL/Transcendental.thy	Thu Mar 05 17:30:29 2015 +0000
@@ -1011,22 +1011,22 @@
   by (rule DERIV_exp [THEN DERIV_isCont])
 
 lemma isCont_exp' [simp]:
-  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
+  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
   by (rule isCont_o2 [OF _ isCont_exp])
 
 lemma tendsto_exp [tendsto_intros]:
-  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
+  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
   shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
   by (rule isCont_tendsto_compose [OF isCont_exp])
 
 lemma continuous_exp [continuous_intros]:
-  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
+  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
   unfolding continuous_def by (rule tendsto_exp)
 
 lemma continuous_on_exp [continuous_intros]:
-  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
+  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
   unfolding continuous_on_def by (auto intro: tendsto_exp)
 
@@ -1106,6 +1106,9 @@
   shows "exp (x + y) = exp x * exp y"
   by (rule exp_add_commuting) (simp add: ac_simps)
 
+lemma exp_double: "exp(2 * z) = exp z ^ 2"
+  by (simp add: exp_add_commuting mult_2 power2_eq_square)
+
 lemmas mult_exp_exp = exp_add [symmetric]
 
 lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
@@ -1136,6 +1139,14 @@
   shows "exp (x - y) = exp x / exp y"
   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
 
+lemma exp_of_nat_mult:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "exp(of_nat n * x) = exp(x) ^ n"
+    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
+
+lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
+  by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
+
 
 subsubsection {* Properties of the Exponential Function on Reals *}
 
@@ -1160,9 +1171,10 @@
 lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
   by simp
 
-lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
+(*FIXME: superseded by exp_of_nat_mult*) 
+lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
   by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
-
+  
 text {* Strict monotonicity of exponential. *}
 
 lemma exp_ge_add_one_self_aux: 
@@ -1481,6 +1493,36 @@
   thus ?thesis unfolding exp_first_two_terms by auto
 qed
 
+corollary exp_half_le2: "exp(1/2) \<le> (2::real)"
+  using exp_bound [of "1/2"]
+  by (simp add: field_simps)
+
+lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
+  by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
+
+lemma exp_bound_lemma:
+  assumes "norm(z) \<le> 1/2" shows "norm(exp z) \<le> 1 + 2 * norm(z)"
+proof -
+  have n: "(norm z)\<^sup>2 \<le> norm z * 1"
+    unfolding power2_eq_square
+    apply (rule mult_left_mono)
+    using assms
+    apply (auto simp: )
+    done
+  show ?thesis
+    apply (rule order_trans [OF norm_exp])
+    apply (rule order_trans [OF exp_bound])
+    using assms n
+    apply (auto simp: )
+    done
+qed
+
+lemma real_exp_bound_lemma:
+  fixes x :: real
+  shows "0 \<le> x \<Longrightarrow> x \<le> 1/2 \<Longrightarrow> exp(x) \<le> 1 + 2 * x"
+using exp_bound_lemma [of x]
+by simp
+
 lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
 proof -
   assume a: "0 <= (x::real)" and b: "x < 1"
@@ -1736,6 +1778,16 @@
   by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
      (auto intro: eventually_gt_at_top)
 
+lemma lim_exp_minus_1:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)"
+proof -
+  have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
+    by (intro derivative_eq_intros | simp)+
+  then show ?thesis
+    by (simp add: Deriv.DERIV_iff2)
+qed
+
 lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
      (auto simp: eventually_at_filter)