merged

--- a/NEWS	Sun Sep 04 19:36:19 2011 +0200
+++ b/NEWS	Sun Sep 04 20:37:20 2011 +0200
@@ -277,6 +277,8 @@
   realpow_two_diff ~> square_diff_square_factored
   reals_complete2 ~> complete_real
   exp_ln_eq ~> ln_unique
+  expi_add ~> exp_add
+  expi_zero ~> exp_zero
   lemma_DERIV_subst ~> DERIV_cong
   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
   LIMSEQ_const ~> tendsto_const
@@ -296,6 +298,9 @@
   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
   LIMSEQ_imp_rabs ~> tendsto_rabs
+  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
+  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
+  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
   LIM_ident ~> tendsto_ident_at
   LIM_const ~> tendsto_const
   LIM_add ~> tendsto_add

--- a/src/HOL/Complex.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/Complex.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -606,7 +606,7 @@
 abbreviation expi :: "complex \<Rightarrow> complex"
   where "expi \<equiv> exp"
 
-lemma expi_imaginary: "expi (Complex 0 b) = cis b"
+lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
 proof (rule complex_eqI)
   { fix n have "Complex 0 b ^ n =
     real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
@@ -614,23 +614,18 @@
       apply (simp add: cos_coeff_def sin_coeff_def)
       apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
       done } note * = this
-  show "Re (exp (Complex 0 b)) = Re (cis b)"
+  show "Re (cis b) = Re (exp (Complex 0 b))"
     unfolding exp_def cis_def cos_def
     by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
       simp add: * mult_assoc [symmetric])
-  show "Im (exp (Complex 0 b)) = Im (cis b)"
+  show "Im (cis b) = Im (exp (Complex 0 b))"
     unfolding exp_def cis_def sin_def
     by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
       simp add: * mult_assoc [symmetric])
 qed
 
 lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
-proof -
-  have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
-    by simp
-  thus ?thesis
-    unfolding exp_add exp_of_real expi_imaginary .
-qed
+  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
 
 lemma complex_split_polar:
      "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
@@ -736,12 +731,6 @@
 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
 by (auto simp add: DeMoivre)
 
-lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
-  by (rule exp_add) (* FIXME: redundant *)
-
-lemma expi_zero: "expi (0::complex) = 1"
-  by (rule exp_zero) (* FIXME: redundant *)
-
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])
 apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])

--- a/src/HOL/Int.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/Int.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -162,7 +162,10 @@
     by (simp add: Zero_int_def One_int_def)
 qed
 
-lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
+abbreviation int :: "nat \<Rightarrow> int" where
+  "int \<equiv> of_nat"
+
+lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
 by (induct m) (simp_all add: Zero_int_def One_int_def add)
 
 
@@ -218,7 +221,7 @@
 
 text{*strict, in 1st argument; proof is by induction on k>0*}
 lemma zmult_zless_mono2_lemma:
-     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
+     "(i::int)<j ==> 0<k ==> int k * i < int k * j"
 apply (induct k)
 apply simp
 apply (simp add: left_distrib)
@@ -226,13 +229,13 @@
 apply (simp_all add: add_strict_mono)
 done
 
-lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
+lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
 apply (cases k)
 apply (auto simp add: le add int_def Zero_int_def)
 apply (rule_tac x="x-y" in exI, simp)
 done
 
-lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
+lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
 apply (cases k)
 apply (simp add: less int_def Zero_int_def)
 apply (rule_tac x="x-y" in exI, simp)
@@ -261,7 +264,7 @@
 done
 
 lemma zless_iff_Suc_zadd:
-  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
+  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
 apply (cases z, cases w)
 apply (auto simp add: less add int_def)
 apply (rename_tac a b c d) 
@@ -314,7 +317,7 @@
 done
 
 text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
+lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
 by (induct n) auto
 
 lemma of_int_power:
@@ -400,13 +403,13 @@
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
 
-lemma nat_int [simp]: "nat (of_nat n) = n"
+lemma nat_int [simp]: "nat (int n) = n"
 by (simp add: nat int_def)
 
-lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
 by (cases z) (simp add: nat le int_def Zero_int_def)
 
-corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
+corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
 by simp
 
 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
@@ -431,14 +434,14 @@
 
 lemma nonneg_eq_int:
   fixes z :: int
-  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
+  assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
   shows P
   using assms by (blast dest: nat_0_le sym)
 
-lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
+lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
 by (cases w) (simp add: nat le int_def Zero_int_def, arith)
 
-corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
+corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
 by (simp only: eq_commute [of m] nat_eq_iff)
 
 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
@@ -446,6 +449,12 @@
 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
 done
 
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
+  by (cases x, simp add: nat le int_def le_diff_conv)
+
+lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
+  by (cases x, cases y, simp add: nat le)
+
 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
 by(simp add: nat_eq_iff) arith
 
@@ -464,10 +473,10 @@
 by (cases z, cases z')
   (simp add: nat add minus diff_minus le Zero_int_def)
 
-lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
+lemma nat_zminus_int [simp]: "nat (- int n) = 0"
 by (simp add: int_def minus nat Zero_int_def) 
 
-lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
 by (cases z) (simp add: nat less int_def, arith)
 
 context ring_1
@@ -485,31 +494,31 @@
 
 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
 
-lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
+lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
 by (simp add: order_less_le del: of_nat_Suc)
 
-lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
+lemma negative_zless [iff]: "- (int (Suc n)) < int m"
 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
 
-lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
+lemma negative_zle_0: "- int n \<le> 0"
 by (simp add: minus_le_iff)
 
-lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
+lemma negative_zle [iff]: "- int n \<le> int m"
 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
 
-lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
 by (subst le_minus_iff, simp del: of_nat_Suc)
 
-lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
 by (simp add: int_def le minus Zero_int_def)
 
-lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
+lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
 by (simp add: linorder_not_less)
 
-lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
+lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
 
-lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
+lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
 proof -
   have "(w \<le> z) = (0 \<le> z - w)"
     by (simp only: le_diff_eq add_0_left)
@@ -520,10 +529,10 @@
   finally show ?thesis .
 qed
 
-lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
+lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
 by simp
 
-lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
 by simp
 
 text{*This version is proved for all ordered rings, not just integers!
@@ -534,7 +543,7 @@
      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
-lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
+lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
 apply (cases x)
 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
 apply (rule_tac x="y - Suc x" in exI, arith)
@@ -547,7 +556,7 @@
 whether an integer is negative or not.*}
 
 theorem int_cases [case_names nonneg neg, cases type: int]:
-  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (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)
@@ -556,12 +565,12 @@
 done
 
 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
-     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
+     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   by (cases z) auto
 
 text{*Contributed by Brian Huffman*}
 theorem int_diff_cases:
-  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
+  obtains (diff) m n where "z = int m - int n"
 apply (cases z rule: eq_Abs_Integ)
 apply (rule_tac m=x and n=y in diff)
 apply (simp add: int_def minus add diff_minus)
@@ -938,11 +947,11 @@
   assumes number_of_eq: "number_of k = of_int k"
 
 class number_semiring = number + comm_semiring_1 +
-  assumes number_of_int: "number_of (of_nat n) = of_nat n"
+  assumes number_of_int: "number_of (int n) = of_nat n"
 
 instance number_ring \<subseteq> number_semiring
 proof
-  fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
+  fix n show "number_of (int n) = (of_nat n :: 'a)"
     unfolding number_of_eq by (rule of_int_of_nat_eq)
 qed
 
@@ -1118,7 +1127,7 @@
   show ?thesis
   proof
     assume eq: "1 + z + z = 0"
-    have "(0::int) < 1 + (of_nat n + of_nat n)"
+    have "(0::int) < 1 + (int n + int n)"
       by (simp add: le_imp_0_less add_increasing) 
     also have "... = - (1 + z + z)" 
       by (simp add: neg add_assoc [symmetric]) 
@@ -1638,7 +1647,7 @@
 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
 
 lemma split_nat [arith_split]:
-  "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L & ?R)")
 proof (cases "i < 0")
   case True thus ?thesis by auto
@@ -1731,11 +1740,6 @@
     by (rule wf_subset [OF wf_measure]) 
 qed
 
-abbreviation
-  int :: "nat \<Rightarrow> int"
-where
-  "int \<equiv> of_nat"
-
 (* `set:int': dummy construction *)
 theorem int_ge_induct [case_names base step, induct set: int]:
   fixes i :: int

--- a/src/HOL/NSA/NSComplex.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -613,7 +613,7 @@
 by (simp add: NSDeMoivre_ext)
 
 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
-by transfer (rule expi_add)
+by transfer (rule exp_add)
 
 
 subsection{*@{term hcomplex_of_complex}: the Injection from

--- a/src/HOL/RComplete.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/RComplete.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -336,9 +336,6 @@
 lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
   unfolding natfloor_def by simp
 
-lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
-  by simp (* TODO: move to Int.thy *)
-
 lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
   unfolding natfloor_def by (intro nat_mono floor_mono)
 
@@ -474,19 +471,16 @@
 lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   unfolding natceiling_def by (intro nat_mono ceiling_mono)
 
-lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
-  by auto (* TODO: move to Int.thy *)
-
 lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)
 
-lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
-  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
+lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
+  unfolding natceiling_def real_of_nat_def
   by (simp add: nat_le_iff ceiling_le_iff)
 
 lemma natceiling_le_eq_number_of [simp]:
-    "~ neg((number_of n)::int) ==> 0 <= x ==>
+    "~ neg((number_of n)::int) ==>
       (natceiling x <= number_of n) = (x <= number_of n)"
   by (simp add: natceiling_le_eq)
 

--- a/src/HOL/SEQ.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/SEQ.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -380,22 +380,6 @@
   shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
 unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
 
-lemma LIMSEQ_add_const: (* FIXME: delete *)
-  fixes a :: "'a::real_normed_vector"
-  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
-by (intro tendsto_intros)
-
-(* FIXME: delete *)
-lemma LIMSEQ_add_minus:
-  fixes a b :: "'a::real_normed_vector"
-  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
-by (intro tendsto_intros)
-
-lemma LIMSEQ_diff_const: (* FIXME: delete *)
-  fixes a b :: "'a::real_normed_vector"
-  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
-by (intro tendsto_intros)
-
 lemma LIMSEQ_diff_approach_zero:
   fixes L :: "'a::real_normed_vector"
   shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
@@ -438,7 +422,8 @@
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus:
      "(%n. r + -inverse(real(Suc n))) ----> r"
-  using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
+  using tendsto_add [OF tendsto_const
+    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"

--- a/src/HOL/Series.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/Series.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -122,7 +122,7 @@
   shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   apply (unfold sums_def)
   apply (simp add: sumr_offset)
-  apply (rule LIMSEQ_diff_const)
+  apply (rule tendsto_diff [OF _ tendsto_const])
   apply (rule LIMSEQ_ignore_initial_segment)
   apply assumption
 done
@@ -166,7 +166,7 @@
 proof -
   from sumSuc[unfolded sums_def]
   have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
-  from LIMSEQ_add_const[OF this, where b="f 0"]
+  from tendsto_add[OF this tendsto_const, where b="f 0"]
   have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
   thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
 qed
@@ -625,7 +625,7 @@
  apply (simp add:diff_Suc split:nat.splits)
  apply (blast intro: norm_ratiotest_lemma)
 apply (rule_tac x = "Suc N" in exI, clarify)
-apply(simp cong:setsum_ivl_cong)
+apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
 done
 
 lemma ratio_test:

--- a/src/HOL/Transcendental.thy	Sun Sep 04 19:36:19 2011 +0200
+++ b/src/HOL/Transcendental.thy	Sun Sep 04 20:37:20 2011 +0200
@@ -1999,7 +1999,7 @@
 apply (drule tan_total_pos)
 apply (cut_tac [2] y="-y" in tan_total_pos, safe)
 apply (rule_tac [3] x = "-x" in exI)
-apply (auto intro!: exI)
+apply (auto del: exI intro!: exI)
 done
 
 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
@@ -2009,7 +2009,7 @@
 apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
 apply (rule_tac [4] Rolle)
 apply (rule_tac [2] Rolle)
-apply (auto intro!: DERIV_tan DERIV_isCont exI
+apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
             simp add: differentiable_def)
 txt{*Now, simulate TRYALL*}
 apply (rule_tac [!] DERIV_tan asm_rl)
@@ -2785,7 +2785,7 @@
         have "norm (?diff 1 n - 0) < r" by auto }
       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
     qed
-    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
+    from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)