# HG changeset patch
# User huffman
# Date 1179896418 -7200
# Node ID ffef77eed382a5eeef37b7b42274b68e6b2bb870
# Parent  636cda81978aa87c2dfe4507587da9e29fe38913
generalize powerseries and termdiffs lemmas using axclasses

diff -r 636cda81978a -r ffef77eed382 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed May 23 02:50:19 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed May 23 07:00:18 2007 +0200
@@ -13,51 +13,53 @@
 
 subsection{*Properties of Power Series*}
 
-lemma lemma_realpow_diff [rule_format (no_asm)]:
-     "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
-apply (induct "n", auto)
-apply (subgoal_tac "p = Suc n")
-apply (simp (no_asm_simp), auto)
-apply (drule sym)
-apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] 
-       del: realpow_Suc)
-done
+lemma lemma_realpow_diff:
+  fixes y :: "'a::recpower"
+  shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
+proof -
+  assume "p \<le> n"
+  hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
+  thus ?thesis by (simp add: power_Suc power_commutes)
+qed
 
 lemma lemma_realpow_diff_sumr:
-     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
-      y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
+  fixes y :: "'a::{recpower,comm_semiring_0}" shows
+     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
+      y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
 by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac
   simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
 
 lemma lemma_realpow_diff_sumr2:
+  fixes y :: "'a::{recpower,comm_ring}" shows
      "x ^ (Suc n) - y ^ (Suc n) =  
-      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
-apply (induct "n", simp)
-apply (auto simp del: setsum_op_ivl_Suc)
+      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
+apply (induct "n", simp add: power_Suc)
+apply (simp add: power_Suc del: setsum_op_ivl_Suc)
 apply (subst setsum_op_ivl_Suc)
-apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc)
+apply (subst lemma_realpow_diff_sumr)
+apply (simp add: right_distrib del: setsum_op_ivl_Suc)
+apply (subst mult_left_commute [where a="x - y"])
+apply (erule subst)
+apply (simp add: power_Suc ring_eq_simps)
 done
 
 lemma lemma_realpow_rev_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
-      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
-apply (case_tac "x = y")
-apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc)
-apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
-apply (rule_tac [2] minus_minus [THEN subst], simp)
-apply (subst minus_mult_left)
-apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc)
+      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
+apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
+apply (rule inj_onI, simp)
+apply auto
+apply (rule_tac x="n - x" in image_eqI, simp, simp)
 done
 
 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>"}.*}
 
 lemma powser_insidea:
-  fixes x z :: real
+  fixes x z :: "'a::{real_normed_field,banach,recpower}"
   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
-  assumes 2: "\<bar>z\<bar> < \<bar>x\<bar>"
-  shows "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)"
+  assumes 2: "norm z < norm x"
+  shows "summable (\<lambda>n. norm (f n * z ^ n))"
 proof -
   from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
   from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
@@ -68,53 +70,55 @@
     by (simp add: Cauchy_convergent_iff)
   hence "Bseq (\<lambda>n. f n * x ^ n)"
     by (rule Cauchy_Bseq)
-  then obtain K where 3: "0 < K" and 4: "\<forall>n. \<bar>f n * x ^ n\<bar> \<le> K"
+  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
     by (simp add: Bseq_def, safe)
-  have "\<exists>N. \<forall>n\<ge>N. norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>"
+  have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
+                   K * norm (z ^ n) * inverse (norm (x ^ n))"
   proof (intro exI allI impI)
     fix n::nat assume "0 \<le> n"
-    have "norm (\<bar>f n\<bar> * z ^ n) * \<bar>x ^ n\<bar> = \<bar>f n * x ^ n\<bar> * \<bar>z ^ n\<bar>"
-      by (simp add: abs_mult)
-    also have "\<dots> \<le> K * \<bar>z ^ n\<bar>"
-      by (simp only: mult_right_mono 4 abs_ge_zero)
-    also have "\<dots> = K * \<bar>z ^ n\<bar> * (inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>)"
+    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
+          norm (f n * x ^ n) * norm (z ^ n)"
+      by (simp add: norm_mult abs_mult)
+    also have "\<dots> \<le> K * norm (z ^ n)"
+      by (simp only: mult_right_mono 4 norm_ge_zero)
+    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
       by (simp add: x_neq_0)
-    also have "\<dots> = K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>"
+    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
       by (simp only: mult_assoc)
-    finally show "norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>"
+    finally show "norm (norm (f n * z ^ n)) \<le>
+                  K * norm (z ^ n) * inverse (norm (x ^ n))"
       by (simp add: mult_le_cancel_right x_neq_0)
   qed
-  moreover have "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)"
+  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   proof -
-    from 2 have "norm \<bar>z * inverse x\<bar> < 1"
-      by (simp add: abs_mult divide_inverse [symmetric])
-    hence "summable (\<lambda>n. \<bar>z * inverse x\<bar> ^ n)"
+    from 2 have "norm (norm (z * inverse x)) < 1"
+      using x_neq_0
+      by (simp add: nonzero_norm_divide divide_inverse [symmetric])
+    hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
       by (rule summable_geometric)
-    hence "summable (\<lambda>n. K * \<bar>z * inverse x\<bar> ^ n)"
+    hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
       by (rule summable_mult)
-    thus "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)"
-      by (simp add: abs_mult power_mult_distrib power_abs
-                    power_inverse mult_assoc)
+    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
+      using x_neq_0
+      by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
+                    power_inverse norm_power mult_assoc)
   qed
-  ultimately show "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)"
+  ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
     by (rule summable_comparison_test)
 qed
 
 lemma powser_inside:
-  fixes f :: "nat \<Rightarrow> real" shows
-     "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |]  
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows
+     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
       ==> summable (%n. f(n) * (z ^ n))"
-apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea, simp)
-apply (rule summable_rabs_cancel)
-apply (simp add: abs_mult power_abs [symmetric])
-done
+by (rule powser_insidea [THEN summable_norm_cancel])
 
 
 subsection{*Term-by-Term Differentiability of Power Series*}
 
 definition
-  diffs :: "(nat => real) => nat => real" where
-  "diffs c = (%n. real (Suc n) * c(Suc n))"
+  diffs :: "(nat => 'a::ring_1) => nat => 'a" where
+  "diffs c = (%n. of_nat (Suc n) * c(Suc n))"
 
 text{*Lemma about distributing negation over it*}
 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
@@ -123,24 +127,24 @@
 text{*Show that we can shift the terms down one*}
 lemma lemma_diffs:
      "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =  
-      (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) +  
-      (real n * c(n) * x ^ (n - Suc 0))"
+      (\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) +  
+      (of_nat n * c(n) * x ^ (n - Suc 0))"
 apply (induct "n")
 apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
 done
 
 lemma lemma_diffs2:
-     "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) =  
+     "(\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) =  
       (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -  
-      (real n * c(n) * x ^ (n - Suc 0))"
+      (of_nat n * c(n) * x ^ (n - Suc 0))"
 by (auto simp add: lemma_diffs)
 
 
 lemma diffs_equiv:
      "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
-      (%n. real n * c(n) * (x ^ (n - Suc 0))) sums  
+      (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums  
          (\<Sum>n. (diffs c)(n) * (x ^ n))"
-apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0")
+apply (subgoal_tac " (%n. of_nat n * c (n) * (x ^ (n - Suc 0))) ----> 0")
 apply (rule_tac [2] LIMSEQ_imp_Suc)
 apply (drule summable_sums) 
 apply (auto simp add: sums_def)
@@ -150,8 +154,9 @@
 done
 
 lemma lemma_termdiff1:
+  fixes z :: "'a :: {recpower,comm_ring}" shows
   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
-   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
+   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
   cong: strong_setsum_cong)
 
@@ -161,20 +166,25 @@
 lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)"
 by arith
 
+lemma sumr_diff_mult_const2:
+  "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
+by (simp add: setsum_subtractf)
+
 lemma lemma_termdiff2:
+  fixes h :: "'a :: {recpower,field,division_by_zero}"
   assumes h: "h \<noteq> 0" shows
-  "((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0) =
+  "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
    h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
-        (z + h) ^ q * z ^ (n - 2 - q))"
-apply (rule real_mult_left_cancel [OF h, THEN iffD1])
+        (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
+apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
 apply (simp add: right_diff_distrib diff_divide_distrib h)
 apply (simp add: mult_assoc [symmetric])
 apply (cases "n", simp)
 apply (simp add: lemma_realpow_diff_sumr2 h
                  right_diff_distrib [symmetric] mult_assoc
-            del: realpow_Suc setsum_op_ivl_Suc)
+            del: realpow_Suc setsum_op_ivl_Suc of_nat_Suc)
 apply (subst lemma_realpow_rev_sumr)
-apply (subst sumr_diff_mult_const)
+apply (subst sumr_diff_mult_const2)
 apply simp
 apply (simp only: lemma_termdiff1 setsum_right_distrib)
 apply (rule setsum_cong [OF refl])
@@ -187,174 +197,185 @@
 done
 
 lemma real_setsum_nat_ivl_bounded2:
-  "\<lbrakk>\<And>p::nat. p < n \<Longrightarrow> f p \<le> K; 0 \<le> K\<rbrakk>
-   \<Longrightarrow> setsum f {0..<n-k} \<le> real n * K"
-apply (rule order_trans [OF real_setsum_nat_ivl_bounded mult_right_mono])
-apply simp_all
+  fixes K :: "'a::ordered_semidom"
+  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
+  assumes K: "0 \<le> K"
+  shows "setsum f {0..<n-k} \<le> of_nat n * K"
+apply (rule order_trans [OF setsum_mono])
+apply (rule f, simp)
+apply (simp add: mult_right_mono K)
 done
 
 lemma lemma_termdiff3:
+  fixes h z :: "'a::{real_normed_field,recpower,division_by_zero}"
   assumes 1: "h \<noteq> 0"
-  assumes 2: "\<bar>z\<bar> \<le> K"
-  assumes 3: "\<bar>z + h\<bar> \<le> K"
-  shows "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar>
-          \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
+  assumes 2: "norm z \<le> K"
+  assumes 3: "norm (z + h) \<le> K"
+  shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
+          \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
 proof -
-  have "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar> =
-        \<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
-          (z + h) ^ q * z ^ (n - 2 - q)\<bar> * \<bar>h\<bar>"
+  have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
+        norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
+          (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
     apply (subst lemma_termdiff2 [OF 1])
-    apply (subst abs_mult)
+    apply (subst norm_mult)
     apply (rule mult_commute)
     done
-  also have "\<dots> \<le> real n * (real (n - Suc 0) * K ^ (n - 2)) * \<bar>h\<bar>"
-  proof (rule mult_right_mono [OF _ abs_ge_zero])
-    from abs_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
-    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> \<bar>(z + h) ^ i * z ^ j\<bar> \<le> K ^ n"
+  also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
+  proof (rule mult_right_mono [OF _ norm_ge_zero])
+    from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans)
+    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
       apply (erule subst)
-      apply (simp only: abs_mult power_abs power_add)
-      apply (intro mult_mono power_mono 2 3 abs_ge_zero zero_le_power K)
+      apply (simp only: norm_mult norm_power power_add)
+      apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
       done
-    show "\<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
-              (z + h) ^ q * z ^ (n - 2 - q)\<bar>
-          \<le> real n * (real (n - Suc 0) * K ^ (n - 2))"
+    show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
+              (z + h) ^ q * z ^ (n - 2 - q))
+          \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
       apply (intro
-         order_trans [OF setsum_abs]
+         order_trans [OF norm_setsum]
          real_setsum_nat_ivl_bounded2
          mult_nonneg_nonneg
-         real_of_nat_ge_zero
+         zero_le_imp_of_nat
          zero_le_power K)
       apply (rule le_Kn, simp)
       done
   qed
-  also have "\<dots> = real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
+  also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
     by (simp only: mult_assoc)
   finally show ?thesis .
 qed
 
 lemma lemma_termdiff4:
+  fixes f :: "'a::{real_normed_field,recpower,division_by_zero} \<Rightarrow>
+              'b::real_normed_vector"
   assumes k: "0 < (k::real)"
-  assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>"
+  assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   shows "f -- 0 --> 0"
 proof (simp add: LIM_def, safe)
   fix r::real assume r: "0 < r"
   have zero_le_K: "0 \<le> K"
     apply (cut_tac k)
-    apply (cut_tac h="k/2" in le, simp, simp)
-    apply (subgoal_tac "0 \<le> K*k", simp add: zero_le_mult_iff) 
-    apply (force intro: order_trans [of _ "\<bar>f (k / 2)\<bar> * 2"]) 
+    apply (cut_tac h="of_real (k/2)" in le, simp)
+    apply (simp del: of_real_divide)
+    apply (drule order_trans [OF norm_ge_zero])
+    apply (simp add: zero_le_mult_iff)
     done
-  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)"
+  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
   proof (cases)
     assume "K = 0"
-    with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < k \<longrightarrow> \<bar>f x\<bar> < r)"
+    with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)"
       by simp
-    thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)" ..
+    thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" ..
   next
     assume K_neq_zero: "K \<noteq> 0"
     with zero_le_K have K: "0 < K" by simp
-    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)"
+    show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
     proof (rule exI, safe)
       from k r K show "0 < min k (r * inverse K / 2)"
         by (simp add: mult_pos_pos positive_imp_inverse_positive)
     next
-      fix x::real
-      assume x1: "x \<noteq> 0" and x2: "\<bar>x\<bar> < min k (r * inverse K / 2)"
-      from x2 have x3: "\<bar>x\<bar> < k" and x4: "\<bar>x\<bar> < r * inverse K / 2"
+      fix x::'a
+      assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)"
+      from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2"
         by simp_all
-      from x1 x3 le have "\<bar>f x\<bar> \<le> K * \<bar>x\<bar>" by simp
-      also from x4 K have "K * \<bar>x\<bar> < K * (r * inverse K / 2)"
+      from x1 x3 le have "norm (f x) \<le> K * norm x" by simp
+      also from x4 K have "K * norm x < K * (r * inverse K / 2)"
         by (rule mult_strict_left_mono)
       also have "\<dots> = r / 2"
         using K_neq_zero by simp
       also have "r / 2 < r"
         using r by simp
-      finally show "\<bar>f x\<bar> < r" .
+      finally show "norm (f x) < r" .
     qed
   qed
 qed
 
 lemma lemma_termdiff5:
+  fixes g :: "'a::{recpower,real_normed_field,division_by_zero} \<Rightarrow>
+              nat \<Rightarrow> 'b::banach"
   assumes k: "0 < (k::real)"
   assumes f: "summable f"
-  assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
+  assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
 proof (rule lemma_termdiff4 [OF k])
-  fix h assume "h \<noteq> 0" and "\<bar>h\<bar> < k"
-  hence A: "\<forall>n. \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
+  fix h::'a assume "h \<noteq> 0" and "norm h < k"
+  hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
     by (simp add: le)
-  hence "\<exists>N. \<forall>n\<ge>N. norm \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>"
+  hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
     by simp
-  moreover from f have B: "summable (\<lambda>n. f n * \<bar>h\<bar>)"
+  moreover from f have B: "summable (\<lambda>n. f n * norm h)"
     by (rule summable_mult2)
-  ultimately have C: "summable (\<lambda>n. \<bar>g h n\<bar>)"
+  ultimately have C: "summable (\<lambda>n. norm (g h n))"
     by (rule summable_comparison_test)
-  hence "\<bar>suminf (g h)\<bar> \<le> (\<Sum>n. \<bar>g h n\<bar>)"
-    by (rule summable_rabs)
-  also from A C B have "(\<Sum>n. \<bar>g h n\<bar>) \<le> (\<Sum>n. f n * \<bar>h\<bar>)"
+  hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
+    by (rule summable_norm)
+  also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
     by (rule summable_le)
-  also from f have "(\<Sum>n. f n * \<bar>h\<bar>) = suminf f * \<bar>h\<bar>"
+  also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
     by (rule suminf_mult2 [symmetric])
-  finally show "\<bar>suminf (g h)\<bar> \<le> suminf f * \<bar>h\<bar>" .
+  finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
 qed
 
 
 text{* FIXME: Long proofs*}
 
 lemma termdiffs_aux:
+  fixes x :: "'a::{recpower,real_normed_field,division_by_zero,banach}"
   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
-  assumes 2: "\<bar>x\<bar> < \<bar>K\<bar>"
+  assumes 2: "norm x < norm K"
   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
-             - real n * x ^ (n - Suc 0))) -- 0 --> 0"
+             - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
 proof -
   from dense [OF 2]
-  obtain r where r1: "\<bar>x\<bar> < r" and r2: "r < \<bar>K\<bar>" by fast
-  from abs_ge_zero r1 have r: "0 < r"
+  obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
+  from norm_ge_zero r1 have r: "0 < r"
     by (rule order_le_less_trans)
   hence r_neq_0: "r \<noteq> 0" by simp
   show ?thesis
   proof (rule lemma_termdiff5)
-    show "0 < r - \<bar>x\<bar>" using r1 by simp
+    show "0 < r - norm x" using r1 by simp
   next
-    from r r2 have "\<bar>r\<bar> < \<bar>K\<bar>"
-      by (simp only: abs_of_nonneg order_less_imp_le)
-    with 1 have "summable (\<lambda>n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))"
+    from r r2 have "norm (of_real r::'a) < norm K"
+      by simp
+    with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
       by (rule powser_insidea)
-    hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. \<bar>c n\<bar>)) n * r ^ n)"
-      by (simp only: diffs_def abs_mult abs_real_of_nat_cancel)
-    hence "summable (\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0))"
+    hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
+      using r
+      by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
+    hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
-    also have "(\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0))
-      = (\<lambda>n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))"
+    also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))
+      = (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
       apply (rule ext)
       apply (simp add: diffs_def)
       apply (case_tac n, simp_all add: r_neq_0)
       done
     finally have "summable 
-      (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * r ^ (n - Suc 0))"
+      (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
     also have
-      "(\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
+      "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
            r ^ (n - Suc 0)) =
-       (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))"
+       (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
       apply (rule ext)
       apply (case_tac "n", simp)
       apply (case_tac "nat", simp)
       apply (simp add: r_neq_0)
       done
     finally show
-      "summable (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))" .
+      "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   next
-    fix h::real and n::nat
+    fix h::'a and n::nat
     assume h: "h \<noteq> 0"
-    assume "\<bar>h\<bar> < r - \<bar>x\<bar>"
-    hence "\<bar>x\<bar> + \<bar>h\<bar> < r" by simp
-    with abs_triangle_ineq have xh: "\<bar>x + h\<bar> < r"
+    assume "norm h < r - norm x"
+    hence "norm x + norm h < r" by simp
+    with norm_triangle_ineq have xh: "norm (x + h) < r"
       by (rule order_le_less_trans)
-    show "\<bar>c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0))\<bar>
-          \<le> \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2) * \<bar>h\<bar>"
-      apply (simp only: abs_mult mult_assoc)
-      apply (rule mult_left_mono [OF _ abs_ge_zero])
+    show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
+          \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
+      apply (simp only: norm_mult mult_assoc)
+      apply (rule mult_left_mono [OF _ norm_ge_zero])
       apply (simp (no_asm) add: mult_assoc [symmetric])
       apply (rule lemma_termdiff3)
       apply (rule h)
@@ -365,23 +386,24 @@
 qed
 
 lemma termdiffs:
+  fixes K x :: "'a::{recpower,real_normed_field,division_by_zero,banach}"
   assumes 1: "summable (\<lambda>n. c n * K ^ n)"
   assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
   assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
-  assumes 4: "\<bar>x\<bar> < \<bar>K\<bar>"
+  assumes 4: "norm x < norm K"
   shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
 proof (simp add: deriv_def, rule LIM_zero_cancel)
   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
             - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   proof (rule LIM_equal2)
-    show "0 < \<bar>K\<bar> - \<bar>x\<bar>" by (simp add: less_diff_eq 4)
+    show "0 < norm K - norm x" by (simp add: less_diff_eq 4)
   next
-    fix h :: real
+    fix h :: 'a
     assume "h \<noteq> 0"
-    assume "norm (h - 0) < \<bar>K\<bar> - \<bar>x\<bar>"
-    hence "\<bar>x\<bar> + \<bar>h\<bar> < \<bar>K\<bar>" by simp
-    hence 5: "\<bar>x + h\<bar> < \<bar>K\<bar>"
-      by (rule abs_triangle_ineq [THEN order_le_less_trans])
+    assume "norm (h - 0) < norm K - norm x"
+    hence "norm x + norm h < norm K" by simp
+    hence 5: "norm (x + h) < norm K"
+      by (rule norm_triangle_ineq [THEN order_le_less_trans])
     have A: "summable (\<lambda>n. c n * x ^ n)"
       by (rule powser_inside [OF 1 4])
     have B: "summable (\<lambda>n. c n * (x + h) ^ n)"
@@ -390,7 +412,7 @@
       by (rule powser_inside [OF 2 4])
     show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h
              - (\<Sum>n. diffs c n * x ^ n) = 
-          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0)))"
+          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
       apply (subst sums_unique [OF diffs_equiv [OF C]])
       apply (subst suminf_diff [OF B A])
       apply (subst suminf_divide [symmetric])
@@ -405,7 +427,7 @@
       done
   next
     show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h -
-               real n * x ^ (n - Suc 0))) -- 0 --> 0"
+               of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
         by (rule termdiffs_aux [OF 3 4])
   qed
 qed
@@ -515,7 +537,8 @@
 
 lemma exp_fdiffs: 
       "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))"
-by (simp add: diffs_def mult_assoc [symmetric] del: mult_Suc)
+by (simp add: diffs_def mult_assoc [symmetric] real_of_nat_def
+         del: mult_Suc of_nat_Suc)
 
 lemma sin_fdiffs: 
       "diffs(%n. if even n then 0  
@@ -524,7 +547,8 @@
                  (- 1) ^ (n div 2)/(real (fact n))  
               else 0)"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse simp del: mult_Suc)
+         simp add: diffs_def divide_inverse real_of_nat_def
+         simp del: mult_Suc of_nat_Suc)
 
 lemma sin_fdiffs2: 
        "diffs(%n. if even n then 0  
@@ -533,7 +557,8 @@
                  (- 1) ^ (n div 2)/(real (fact n))  
               else 0)"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse simp del: mult_Suc)
+         simp add: diffs_def divide_inverse real_of_nat_def
+         simp del: mult_Suc of_nat_Suc)
 
 lemma cos_fdiffs: 
       "diffs(%n. if even n then  
@@ -541,8 +566,8 @@
        = (%n. - (if even n then 0  
            else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
-         simp del: mult_Suc)
+         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
+         simp del: mult_Suc of_nat_Suc)
 
 
 lemma cos_fdiffs2: 
@@ -551,8 +576,8 @@
        = - (if even n then 0  
            else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
 by (auto intro!: ext 
-         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex
-         simp del: mult_Suc)
+         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
+         simp del: mult_Suc of_nat_Suc)
 
 text{*Now at last we can get the derivatives of exp, sin and cos*}