# HG changeset patch
# User huffman
# Date 1176762829 -7200
# Node ID c51667189bd3cd0a0f17657d59a3c1d1b9e50227
# Parent  936f7580937d25cb81b50e07e05458696fcbed6a
lemma geometric_sum no longer needs class division_by_zero

diff -r 936f7580937d -r c51667189bd3 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Tue Apr 17 00:30:44 2007 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Tue Apr 17 00:33:49 2007 +0200
@@ -340,7 +340,7 @@
 lemmas sumr_geometric = geometric_sum [where 'a = real]
 
 lemma geometric_sums:
-  fixes x :: "'a::{real_normed_field,recpower,division_by_zero}"
+  fixes x :: "'a::{real_normed_field,recpower}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) sums (1 / (1 - x))"
 proof -
   assume less_1: "norm x < 1"
@@ -348,8 +348,7 @@
   hence neq_0: "x - 1 \<noteq> 0" by simp
   from less_1 have lim_0: "(\<lambda>n. x ^ n) ----> 0"
     by (rule LIMSEQ_power_zero)
-  hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x
-- 1)"
+  hence "(\<lambda>n. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"
     using neq_0 by (intro LIMSEQ_divide LIMSEQ_diff LIMSEQ_const)
   hence "(\<lambda>n. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"
     by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
@@ -358,7 +357,7 @@
 qed
 
 lemma summable_geometric:
-  fixes x :: "'a::{real_normed_field,recpower,division_by_zero}"
+  fixes x :: "'a::{real_normed_field,recpower}"
   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
 by (rule geometric_sums [THEN sums_summable])