# HG changeset patch
# User wenzelm
# Date 1238094598 -3600
# Node ID 8fe5bf6169e9a8ad9bb873049461be2832114927
# Parent  afca5be252d62607b8352041efe5d0427e6396bd# Parent  461ee3e49ad3bf8518f0d051f89dc6faf4361d04
merged

diff -r 461ee3e49ad3 -r 8fe5bf6169e9 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Mar 26 20:08:55 2009 +0100
+++ b/src/HOL/Power.thy	Thu Mar 26 20:09:58 2009 +0100
@@ -186,6 +186,10 @@
 apply (auto simp add: abs_mult)
 done
 
+lemma abs_power_minus [simp]:
+  fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)"
+  by (simp add: abs_minus_cancel power_abs) 
+
 lemma zero_less_power_abs_iff [simp,noatp]:
      "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
 proof (induct "n")
diff -r 461ee3e49ad3 -r 8fe5bf6169e9 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Thu Mar 26 20:08:55 2009 +0100
+++ b/src/HOL/SEQ.thy	Thu Mar 26 20:09:58 2009 +0100
@@ -40,10 +40,23 @@
 
 definition
   monoseq :: "(nat=>real)=>bool" where
-    --{*Definition for monotonicity*}
+    --{*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.*}
   [code del]: "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
+    --{*Increasing sequence*}
+  [code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
+
+definition
+  decseq :: "(nat=>real)=>bool" where
+    --{*Increasing sequence*}
+  [code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+
+definition
   subseq :: "(nat => nat) => bool" where
     --{*Definition of subsequence*}
   [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
@@ -886,6 +899,14 @@
   thus ?case by arith
 qed
 
+lemma LIMSEQ_subseq_LIMSEQ:
+  "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
+apply (auto simp add: LIMSEQ_def) 
+apply (drule_tac x=r in spec, clarify)  
+apply (rule_tac x=no in exI, clarify) 
+apply (blast intro: seq_suble le_trans dest!: spec) 
+done
+
 subsection {* Bounded Monotonic Sequences *}
 
 
@@ -1021,6 +1042,47 @@
 apply (auto intro!: Bseq_mono_convergent)
 done
 
+subsubsection{*Increasing and Decreasing Series*}
+
+lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
+  by (simp add: incseq_def monoseq_def) 
+
+lemma incseq_le: 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)"
+  thus ?thesis by simp
+next
+  assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
+  hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
+    by (auto simp add: incseq_def intro: order_antisym)
+  have X: "!!n. X n = X 0"
+    by (blast intro: const [of 0]) 
+  have "X = (\<lambda>n. X 0)"
+    by (blast intro: ext X)
+  hence "L = X 0" using LIMSEQ_const [of "X 0"]
+    by (auto intro: LIMSEQ_unique lim) 
+  thus ?thesis
+    by (blast intro: eq_refl X)
+qed
+
+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)" 
+  by (simp add: decseq_def incseq_def)
+
+
+lemma decseq_le: 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)
+  have "- X n \<le> - L" 
+    by (blast intro: incseq_le [OF inc] LIMSEQ_minus lim) 
+  thus ?thesis
+    by simp
+qed
+
 subsubsection{*A Few More Equivalence Theorems for Boundedness*}
 
 text{*alternative formulation for boundedness*}
@@ -1065,6 +1127,14 @@
   "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
 by (simp add: Cauchy_def)
 
+lemma Cauchy_subseq_Cauchy:
+  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
+apply (auto simp add: Cauchy_def) 
+apply (drule_tac x=e in spec, clarify)  
+apply (rule_tac x=M in exI, clarify) 
+apply (blast intro: seq_suble le_trans dest!: spec) 
+done
+
 subsubsection {* Cauchy Sequences are Bounded *}
 
 text{*A Cauchy sequence is bounded -- this is the standard
@@ -1238,6 +1308,11 @@
   shows "Cauchy X = convergent X"
 by (fast intro: Cauchy_convergent convergent_Cauchy)
 
+lemma convergent_subseq_convergent:
+  fixes X :: "nat \<Rightarrow> 'a::banach"
+  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
+  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) 
+
 
 subsection {* Power Sequences *}
 
diff -r 461ee3e49ad3 -r 8fe5bf6169e9 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Thu Mar 26 20:08:55 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML	Thu Mar 26 20:09:58 2009 +0100
@@ -377,6 +377,8 @@
 struct
   val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   val eq_reflection = eq_reflection
+  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
+    | is_numeral _ = false;
 end;
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
diff -r 461ee3e49ad3 -r 8fe5bf6169e9 src/Provers/Arith/assoc_fold.ML
--- a/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 20:08:55 2009 +0100
+++ b/src/Provers/Arith/assoc_fold.ML	Thu Mar 26 20:09:58 2009 +0100
@@ -12,6 +12,7 @@
 sig
   val assoc_ss: simpset
   val eq_reflection: thm
+  val is_numeral: term -> bool
 end;
 
 signature ASSOC_FOLD =
@@ -29,10 +30,9 @@
 
 (*Separate the literals from the other terms being combined*)
 fun sift_terms plus (t, (lits,others)) =
+  if Data.is_numeral t then (t::lits, others) (*new literal*) else
   (case t of
-    Const (@{const_name Int.number_of}, _) $ _ =>       (* FIXME logic dependent *)
-      (t::lits, others)         (*new literal*)
-  | (f as Const _) $ x $ y =>
+    (f as Const _) $ x $ y =>
       if f = plus
       then sift_terms plus (x, sift_terms plus (y, (lits,others)))
       else (lits, t::others)    (*arbitrary summand*)