# HG changeset patch
# User haftmann
# Date 1292950355 -3600
# Node ID a35af5180c0104ff62507e68735a2b5a929f147b
# Parent  17b09240893cb3046f6914c171500bd6ef6d135b# Parent  48503e4e96b67891d43c7644c924b6350a9367d6
merged

diff -r 48503e4e96b6 -r a35af5180c01 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Dec 21 17:52:23 2010 +0100
+++ b/src/HOL/Deriv.thy	Tue Dec 21 17:52:35 2010 +0100
@@ -879,14 +879,14 @@
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
   apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
-  apply (auto simp add: DERIV_minus) 
+  apply (auto simp add: DERIV_minus)
   done
 
 lemma DERIV_neg_dec_right:
   fixes f :: "real => real"
   shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
   apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
-  apply (auto simp add: DERIV_minus) 
+  apply (auto simp add: DERIV_minus)
   done
 
 lemma DERIV_local_max:
@@ -1554,21 +1554,8 @@
   then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
 
   from cdef have "DERIV ?h c :> l" by auto
-  moreover
-  {
-    have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
-      apply (insert DERIV_const [where k="f b - f a"])
-      apply (drule meta_spec [of _ c])
-      apply (drule DERIV_mult [OF _ g'cdef])
-      by simp
-    moreover have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
-      apply (insert DERIV_const [where k="g b - g a"])
-      apply (drule meta_spec [of _ c])
-      apply (drule DERIV_mult [OF _ f'cdef])
-      by simp
-    ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
-      by (simp add: DERIV_diff)
-  }
+  moreover have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
+    using g'cdef f'cdef by (auto intro!: DERIV_intros)
   ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
 
   {
diff -r 48503e4e96b6 -r a35af5180c01 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 17:52:23 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 17:52:35 2010 +0100
@@ -33,7 +33,7 @@
 apply (rule finite_deflation_approx)
 done
 
-lemma compact_approx: "compact (approx n\<cdot>x)"
+lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
 apply (rule finite_deflation.compact)
 apply (rule finite_deflation_approx)
 done
diff -r 48503e4e96b6 -r a35af5180c01 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Tue Dec 21 17:52:23 2010 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Tue Dec 21 17:52:35 2010 +0100
@@ -250,9 +250,13 @@
 typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
 by auto
 
-lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
+lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
 
+lemma Abs_compact_basis_inverse' [simp]:
+   "compact x \<Longrightarrow> Rep_compact_basis (Abs_compact_basis x) = x"
+by (rule Abs_compact_basis_inverse [unfolded mem_Collect_eq])
+
 instantiation compact_basis :: (pcpo) below
 begin
 
@@ -276,7 +280,7 @@
   "compact_bot = Abs_compact_basis \<bottom>"
 
 lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \<bottom>"
-unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
+unfolding compact_bot_def by simp
 
 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
 unfolding compact_le_def Rep_compact_bot by simp
@@ -419,7 +423,7 @@
 
 lemma Rep_cb_take:
   "Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)"
-by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx)
+by (simp add: cb_take.simps(2))
 
 lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric]
 
@@ -428,7 +432,7 @@
 apply (simp add: Rep_compact_basis_inject [symmetric])
 apply (simp add: Rep_cb_take)
 apply (rule compact_eq_approx)
-apply (rule compact_Rep_compact_basis)
+apply (rule Rep_compact_basis')
 done
 
 lemma cb_take_less: "cb_take n x \<sqsubseteq> x"
@@ -783,61 +787,49 @@
   fix w :: "'a"
   show "below.ideal (approximants w)"
   proof (rule below.idealI)
-    show "\<exists>x. x \<in> approximants w"
-      unfolding approximants_def
-      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
-      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
-      done
+    have "Abs_compact_basis (approx 0\<cdot>w) \<in> approximants w"
+      by (simp add: approximants_def approx_below)
+    thus "\<exists>x. x \<in> approximants w" ..
   next
     fix x y :: "'a compact_basis"
-    assume "x \<in> approximants w" "y \<in> approximants w"
-    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-      unfolding approximants_def
-      apply simp
-      apply (cut_tac a=x in compact_Rep_compact_basis)
-      apply (cut_tac a=y in compact_Rep_compact_basis)
-      apply (drule compact_eq_approx)
-      apply (drule compact_eq_approx)
-      apply (clarify, rename_tac i j)
-      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
-      apply (simp add: compact_le_def)
-      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
-      apply (erule subst, erule subst)
-      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
-      done
+    assume x: "x \<in> approximants w" and y: "y \<in> approximants w"
+    obtain i where i: "approx i\<cdot>(Rep_compact_basis x) = Rep_compact_basis x"
+      using compact_eq_approx Rep_compact_basis' by fast
+    obtain j where j: "approx j\<cdot>(Rep_compact_basis y) = Rep_compact_basis y"
+      using compact_eq_approx Rep_compact_basis' by fast
+    let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)"
+    have "?z \<in> approximants w"
+      by (simp add: approximants_def approx_below)
+    moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
+      by (simp add: approximants_def compact_le_def)
+         (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
+    ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
   next
     fix x y :: "'a compact_basis"
     assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
-      unfolding approximants_def
-      apply simp
-      apply (simp add: compact_le_def)
-      apply (erule (1) below_trans)
-      done
+      unfolding approximants_def compact_le_def
+      by (auto elim: below_trans)
   qed
 next
   fix Y :: "nat \<Rightarrow> 'a"
-  assume Y: "chain Y"
-  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
+  assume "chain Y"
+  thus "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
     unfolding approximants_def
-    apply safe
-    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
-    apply (erule below_lub [OF Y])
-    done
+    by (auto simp add: compact_below_lub_iff)
 next
   fix a :: "'a compact_basis"
   show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
     unfolding approximants_def compact_le_def ..
 next
   fix x y :: "'a"
-  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
-    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y")
-    apply (simp add: lub_distribs)
-    apply (rule admD, simp, simp)
-    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
-    apply (simp add: approximants_def Abs_compact_basis_inverse
-                     approx_below compact_approx)
-    apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx)
-    done
+  assume "approximants x \<subseteq> approximants y"
+  hence "\<forall>z. compact z \<longrightarrow> z \<sqsubseteq> x \<longrightarrow> z \<sqsubseteq> y"
+    by (simp add: approximants_def subset_eq)
+       (metis Abs_compact_basis_inverse')
+  hence "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y"
+    by (simp add: lub_below approx_below)
+  thus "x \<sqsubseteq> y"
+    by (simp add: lub_distribs)
 next
   show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f"
     by (rule exI, rule inj_place)
diff -r 48503e4e96b6 -r a35af5180c01 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Dec 21 17:52:23 2010 +0100
+++ b/src/HOL/SEQ.thy	Tue Dec 21 17:52:35 2010 +0100
@@ -34,27 +34,27 @@
   "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
 
 definition
-  monoseq :: "(nat=>real)=>bool" where
-    --{*Definition of monotonicity. 
-        The use of disjunction here complicates proofs considerably. 
-        One alternative is to add a Boolean argument to indicate the direction. 
+  monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+    --{*Definition of monotonicity.
+        The use of disjunction here complicates proofs considerably.
+        One alternative is to add a Boolean argument to indicate the direction.
         Another is to develop the notions of increasing and decreasing first.*}
   "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
 
 definition
-  incseq :: "(nat=>real)=>bool" where
+  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
     --{*Increasing sequence*}
-  "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
+  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
 
 definition
-  decseq :: "(nat=>real)=>bool" where
-    --{*Increasing sequence*}
-  "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+    --{*Decreasing sequence*}
+  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
 
 definition
-  subseq :: "(nat => nat) => bool" where
+  subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
     --{*Definition of subsequence*}
-  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+  "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
 
 definition
   Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
@@ -502,22 +502,6 @@
     qed
 qed
 
-text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
-
-lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
-  unfolding Ex1_def
-  apply (rule_tac x="nat_rec e f" in exI)
-  apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply simp
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
 text{*Subsequence (alternative definition, (e.g. Hoskins)*}
 
 lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
@@ -528,8 +512,7 @@
 done
 
 lemma monoseq_Suc:
-   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
-                 | (\<forall>n. X (Suc n) \<le> X n))"
+  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
 apply (simp add: monoseq_def)
 apply (auto dest!: le_imp_less_or_eq)
 apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
@@ -552,7 +535,9 @@
 lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
 by (simp add: monoseq_Suc)
 
-lemma monoseq_minus: assumes "monoseq a"
+lemma monoseq_minus:
+  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
+  assumes "monoseq a"
   shows "monoseq (\<lambda> n. - a n)"
 proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
   case True
@@ -564,7 +549,9 @@
   thus ?thesis by (rule monoI1)
 qed
 
-lemma monoseq_le: assumes "monoseq a" and "a ----> x"
+lemma monoseq_le:
+  fixes a :: "nat \<Rightarrow> real"
+  assumes "monoseq a" and "a ----> x"
   shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> 
          ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
 proof -
@@ -615,121 +602,48 @@
   qed auto
 qed
 
-text{* for any sequence, there is a mootonic subsequence *}
-lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
-proof-
-  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
-    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
-    from nat_function_unique[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
-    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
-    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
-      using H apply - 
-      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
-      unfolding order_le_less by blast 
-    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
-    {fix n
-      have "?P (f (Suc n)) (f n)" 
-        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
-        using H apply - 
-      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
-      unfolding order_le_less by blast 
-    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
-  note fSuc = this
-    {fix p q assume pq: "p \<ge> f q"
-      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
-        by (cases q, simp_all) }
-    note pqth = this
-    {fix q
-      have "f (Suc q) > f q" apply (induct q) 
-        using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
-    note fss = this
-    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
-    {fix a b 
-      have "f a \<le> f (a + b)"
-      proof(induct b)
-        case 0 thus ?case by simp
-      next
-        case (Suc b)
-        from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
-      qed}
-    note fmon0 = this
-    have "monoseq (\<lambda>n. s (f n))" 
-    proof-
-      {fix n
-        have "s (f n) \<ge> s (f (Suc n))" 
-        proof(cases n)
-          case 0
-          assume n0: "n = 0"
-          from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
-          from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
-        next
-          case (Suc m)
-          assume m: "n = Suc m"
-          from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
-          from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
-        qed}
-      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
+text{* for any sequence, there is a monotonic subsequence *}
+lemma seq_monosub:
+  fixes s :: "nat => 'a::linorder"
+  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
+proof cases
+  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
+  assume *: "\<forall>n. \<exists>p. ?P p n"
+  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
+  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
+  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
+  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
+  then have "subseq f" unfolding subseq_Suc_iff by auto
+  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
+  proof (intro disjI2 allI)
+    fix n show "s (f (Suc n)) \<le> s (f n)"
+    proof (cases n)
+      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
+    next
+      case (Suc m)
+      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
+      with P_Suc Suc show ?thesis by simp
     qed
-    with th1 have ?thesis by blast}
-  moreover
-  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
-    {fix p assume p: "p \<ge> Suc N" 
-      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
-      have "m \<noteq> p" using m(2) by auto 
-      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
-    note th0 = this
-    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
-    from nat_function_unique[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
-    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
-      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
-    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
-      using N apply - 
-      apply (erule allE[where x="Suc N"], clarsimp)
-      apply (rule_tac x="m" in exI)
-      apply auto
-      apply (subgoal_tac "Suc N \<noteq> m")
-      apply simp
-      apply (rule ccontr, simp)
-      done
-    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
-    {fix n
-      have "f n > N \<and> ?P (f (Suc n)) (f n)"
-        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
-      proof (induct n)
-        case 0 thus ?case
-          using f0 N apply auto 
-          apply (erule allE[where x="f 0"], clarsimp) 
-          apply (rule_tac x="m" in exI, simp)
-          by (subgoal_tac "f 0 \<noteq> m", auto)
-      next
-        case (Suc n)
-        from Suc.hyps have Nfn: "N < f n" by blast
-        from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
-        with Nfn have mN: "m > N" by arith
-        note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
-        
-        from key have th0: "f (Suc n) > N" by simp
-        from N[rule_format, OF th0]
-        obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
-        have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
-        hence "m' > f (Suc n)" using m'(1) by simp
-        with key m'(2) show ?case by auto
-      qed}
-    note fSuc = this
-    {fix n
-      have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto 
-      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
-    note thf = this
-    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
-    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
-      apply -
-      apply (rule disjI1)
-      apply auto
-      apply (rule order_less_imp_le)
-      apply blast
-      done
-    then have ?thesis  using sqf by blast}
-  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
+  qed
+  ultimately show ?thesis by auto
+next
+  let "?P p m" = "m < p \<and> s m < s p"
+  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
+  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
+  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
+  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
+  have P_0: "?P (f 0) (Suc N)"
+    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
+  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
+      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
+  note P' = this
+  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
+      by (induct i) (insert P_0 P', auto) }
+  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
+    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
+  then show ?thesis by auto
 qed
 
 lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
@@ -738,7 +652,7 @@
 next
   case (Suc n)
   from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
-  have "n < f (Suc n)" by arith 
+  have "n < f (Suc n)" by arith
   thus ?case by arith
 qed
 
@@ -887,7 +801,7 @@
 by (simp add: Bseq_def)
 
 text{*Main monotonicity theorem*}
-lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
+lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)"
 apply (simp add: monoseq_def, safe)
 apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
 apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
@@ -897,9 +811,11 @@
 subsubsection{*Increasing and Decreasing Series*}
 
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
-  by (simp add: incseq_def monoseq_def) 
+  by (simp add: incseq_def monoseq_def)
 
-lemma incseq_le: assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
+lemma incseq_le:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
   using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
 proof
   assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
@@ -939,11 +855,13 @@
 lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
   by (simp add: decseq_def monoseq_def)
 
-lemma decseq_eq_incseq: "decseq X = incseq (\<lambda>n. - X n)" 
+lemma decseq_eq_incseq:
+  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
   by (simp add: decseq_def incseq_def)
 
 
-lemma decseq_le: assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
+lemma decseq_le:
+  fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
 proof -
   have inc: "incseq (\<lambda>n. - X n)" using dec
     by (simp add: decseq_eq_incseq)
@@ -1220,7 +1138,7 @@
 apply (auto dest: power_mono)
 done
 
-lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
+lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
 apply (clarify intro!: mono_SucI2)
 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
 done