# HG changeset patch
# User wenzelm
# Date 1292431402 -3600
# Node ID 5645aaee6b3873ba1c622f0079e728bb6a5fdfd1
# Parent  95167879f67526b78d461d8575bce6a923eae50d# Parent  6854e9a40edcae7f6e55d5fdaa8335fcf2ae5eb6
merged

diff -r 6854e9a40edc -r 5645aaee6b38 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Wed Dec 15 15:11:56 2010 +0100
+++ b/src/HOL/MacLaurin.thy	Wed Dec 15 17:43:22 2010 +0100
@@ -19,9 +19,8 @@
     "0 < h ==>
      \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
                (B * ((h^n) / real(fact n)))"
-by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
-                 real(fact n) / (h^n)"
-       in exI, simp)
+by (rule exI[where x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
+                 real(fact n) / (h^n)"]) simp
 
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
@@ -31,142 +30,38 @@
   by (subst fact_reduce_nat, auto)
 
 lemma Maclaurin_lemma2:
+  fixes B
   assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-  and INIT : "n = Suc k"
-  and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) + 
-  B * (t ^ (n - m) / real (fact (n - m)))))"
+    and INIT : "n = Suc k"
+  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
+    B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
   shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
-proof (rule allI)+
-  fix m
-  fix t
-  show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
-  proof
-    assume INIT2: "m < n & 0 \<le> t & t \<le> h"
-    hence INTERV: "0 \<le> t & t \<le> h" ..
-    from INIT2 and INIT have mtok: "m < Suc k" by arith
-    have "DERIV (\<lambda>t. diff m t -
-    ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +
-    B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))
-    t :> diff (Suc m) t -
-    ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
-    B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"
-    proof -
-      from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp
+proof (rule allI impI)+
+  fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
+  have "DERIV (difg m) t :> diff (Suc m) t -
+    ((\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
+     real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
+    by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])
       moreover
-      have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +
-	B * (x ^ (Suc k - m) / real (fact (Suc k - m))))
-	t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
-	B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
-      proof -
-	have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t
-	  :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"
-	proof -
-	  have "\<exists> d. k = m + d"
-	  proof -
-	    from INIT2 have "m < n" ..
-	    hence "\<exists> d. n = m + d + Suc 0" by arith
-	    with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)
-	  qed
-	  from this obtain d where kmd: "k = m + d" ..
-	  have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) +
-            diff m 0)
-	    t :> (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"
-	    
-	  proof - 
-	    have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) + diff m 0) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0"
-	    proof -
-	      from DERIV and INTERV have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma)))) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r))"
-	      proof -
-		have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>
-		  DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
-		  :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
-		proof (rule allI)
-		  fix r
-		  show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>
-		    DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
-		    :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
-		  proof 
-		    assume "0 \<le> r & r < 0 + d"
-		    have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *
-                      (x ^ Suc r * inverse (real (fact (Suc r)))))
-		      t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"
-		    proof -
-                      have "(1 + real r) * real (fact r) \<noteq> 0" by auto
-		      from this have "real (fact r) + real r * real (fact r) \<noteq> 0"
-                        by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)
-                      from this have "DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t :> real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
-			0 * t ^ Suc r"
-                        apply - by ( rule DERIV_intros | rule refl)+ auto
-		      moreover
-		      have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
-			0 * t ^ Suc r =
-			t ^ r * inverse (real (fact r))"
-		      proof -
-			
-			have " real (Suc r) * t ^ (Suc r - Suc 0) *
-			  inverse (real (Suc r) * real (fact r)) +
-			  0 * t ^ Suc r =
-			  t ^ r * inverse (real (fact r))" by (simp add: mult_ac)
-			hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +
-			  0 * t ^ Suc r =
-			  t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)
-			thus ?thesis by (subst fact_Suc)
-		      qed
-		      ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t
-			:> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)
-		      thus ?thesis by (rule DERIV_cmult)
-		    qed
-		    thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /
-                      real (fact (Suc r)))
-		      t :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)" by (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
-		  qed
-		qed
-		thus ?thesis by (rule DERIV_sumr)
-	      qed
-	      moreover
-	      from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .
-	      ultimately show ?thesis by (rule DERIV_add)
-	    qed
-	    moreover
-	    have " (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0 =  (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"  by simp
-	    ultimately show ?thesis by (rule lemma_DERIV_subst)
-	  qed
-	  with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
-	qed
-	moreover
-	have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t
-	  :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
-	proof -
-	  have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t
-	    :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"
-	  proof -
-	    have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)
-	    moreover
-	    have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)
-	    moreover
-	    have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp
-	    ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t
-	      :>  ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
-	      real (fact (Suc k - m)) ^ Suc (Suc 0)"
-              apply -
-              apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto
-	    moreover
-	    from mtok and INIT have "( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
-	      real (fact (Suc k - m)) ^ Suc (Suc 0) =  t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))" by (simp add: fact_diff_Suc)
-	    ultimately show ?thesis by (rule lemma_DERIV_subst)
-	  qed
-	  moreover
-	  thus ?thesis by (rule DERIV_cmult)
-	qed
-	ultimately show ?thesis by (rule DERIV_add)
-      qed
-      ultimately show ?thesis by (rule DERIV_diff) 
-    qed
-    from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify
-  qed
+  from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
+    unfolding atLeast0LessThan[symmetric] by auto
+  have "(\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
+      (\<Sum>x = 0..<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
+    unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
+  moreover
+  have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
+    by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)
+  have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =
+      diff (Suc m + x) 0 * t^x / real (fact x)"
+    by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])
+  moreover
+  have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =
+      B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"
+    using `0 < n - m` by (simp add: fact_reduce_nat)
+  ultimately show "DERIV (difg m) t :> difg (Suc m) t"
+    unfolding difg_def by simp
 qed
 
-
 lemma Maclaurin:
   assumes h: "0 < h"
   assumes n: "0 < n"
@@ -177,19 +72,19 @@
     "\<exists>t. 0 < t & t < h &
               f h =
               setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
-              (diff n t / real (fact n)) * h ^ n"  
+              (diff n t / real (fact n)) * h ^ n"
 proof -
   from n obtain m where m: "n = Suc m"
-    by (cases n, simp add: n)
+    by (cases n) (simp add: n)
 
   obtain B where f_h: "f h =
         (\<Sum>m = 0..<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
         B * (h ^ n / real (fact n))"
     using Maclaurin_lemma [OF h] ..
 
-  obtain g where g_def: "g = (%t. f t -
-    (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}
-      + (B * (t^n / real(fact n)))))" by blast
+  def g \<equiv> "(\<lambda>t. f t -
+    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {0..<n}
+      + (B * (t^n / real(fact n)))))"
 
   have g2: "g 0 = 0 & g h = 0"
     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
@@ -197,16 +92,16 @@
     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
     done
 
-  obtain difg where difg_def: "difg = (%m t. diff m t -
+  def difg \<equiv> "(%m t. diff m t -
     (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m}
-      + (B * ((t ^ (n - m)) / real (fact (n - m))))))" by blast
+      + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
 
   have difg_0: "difg 0 = g"
     unfolding difg_def g_def by (simp add: diff_0)
 
   have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real.
         m < n \<and> (0\<Colon>real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
-    using diff_Suc m difg_def by (rule Maclaurin_lemma2)
+    using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)
 
   have difg_eq_0: "\<forall>m. m < n --> difg m 0 = 0"
     apply clarify
@@ -233,7 +128,7 @@
   have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
   using `m < n`
   proof (induct m)
-  case 0
+    case 0
     show ?case
     proof (rule Rolle)
       show "0 < h" by fact
@@ -244,7 +139,7 @@
         by (simp add: differentiable_difg n)
     qed
   next
-  case (Suc m')
+    case (Suc m')
     hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
     then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
     have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
@@ -276,7 +171,6 @@
       using `difg (Suc m) t = 0`
       by (simp add: m f_h difg_def del: fact_Suc)
   qed
-
 qed
 
 lemma Maclaurin_objl:
@@ -298,11 +192,11 @@
 proof (cases "n")
   case 0 with INIT1 INIT2 show ?thesis by fastsimp
 next
-  case Suc 
+  case Suc
   hence "n > 0" by simp
   from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
     f h =
-    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n" 
+    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
     by (rule Maclaurin)
   thus ?thesis by fastsimp
 qed
@@ -319,49 +213,22 @@
 by (blast intro: Maclaurin2)
 
 lemma Maclaurin_minus:
-  assumes INTERV : "h < 0" and
-  INIT : "0 < n" "diff 0 = f" and
-             ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
+  assumes "h < 0" "0 < n" "diff 0 = f"
+  and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
   shows "\<exists>t. h < t & t < 0 &
          f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
          diff n t / real (fact n) * h ^ n"
 proof -
-  from INTERV have "0 < -h" by simp
-  moreover
-  from INIT have "0 < n" by simp
-  moreover
-  from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp
-  moreover
-  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>
-    DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
-  proof (rule allI impI)+
-    fix m t
-    assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"
-    with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
-    proof -
-      
-      from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)
-      proof -
-	from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force
-	moreover
-	from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus) 
-	ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)
-	thus ?thesis by simp
-      qed
-      thus ?thesis
-      proof -
-	assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)
-	hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)
-	thus ?thesis by simp 
-      qed
-    qed
-  qed
-  ultimately have t_exists: "\<exists>t>0. t < - h \<and>
+  txt "Transform @{text ABL'} into @{text DERIV_intros} format."
+  note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
+  from assms
+  have "\<exists>t>0. t < - h \<and>
     f (- (- h)) =
     (\<Sum>m = 0..<n.
     (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
-    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
-  from this obtain t where t_def: "?P t" ..
+    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
+    by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')
+  then guess t ..
   moreover
   have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
     by (auto simp add: power_mult_distrib[symmetric])
@@ -397,110 +264,61 @@
    diff 0 0 =
    (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
    diff n 0 * 0 ^ n / real (fact n)"
-by (induct "n", auto)
+by (induct "n") auto
 
 lemma Maclaurin_bi_le:
-   assumes INIT : "diff 0 = f"
+   assumes "diff 0 = f"
    and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
    shows "\<exists>t. abs t \<le> abs x &
               f x =
               (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
-              diff n t / real (fact n) * x ^ n"
-proof (cases "n = 0")
-  case True from INIT True show ?thesis by force
+     diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
+proof cases
+  assume "n = 0" with `diff 0 = f` show ?thesis by force
 next
-  case False
-  from this have n_not_zero:"n \<noteq> 0" .
-  from False INIT DERIV show ?thesis
-  proof (cases "x = 0")
-    case True show ?thesis
-    proof -
-      from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
-	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n" by(force simp add: Maclaurin_bi_le_lemma) 
-      thus ?thesis ..
-    qed
+  assume "n \<noteq> 0"
+  show ?thesis
+  proof (cases rule: linorder_cases)
+    assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV
+    have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma)
+    thus ?thesis ..
   next
-    case False 
-    note linorder_less_linear [of "x" "0"] 
-    thus ?thesis
-    proof (elim disjE)
-      assume "x = 0" with False show ?thesis ..
-      next
-      assume x_less_zero: "x < 0" moreover
-      from n_not_zero have "0 < n" by simp moreover
-      have "diff 0 = diff 0" by simp moreover
-      have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-      proof (rule allI, rule allI, rule impI)
-	fix m t
-	assume "m < n & x \<le> t & t \<le> 0"
-	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)
-      qed
-      ultimately have t_exists:"\<exists>t>x. t < 0 \<and>
-        diff 0 x =
-        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
-      from this obtain t where t_def: "?P t" ..
-      from t_def x_less_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
-	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
-	by (simp add: abs_if order_less_le)
-      thus ?thesis by (rule exI)
-    next
-    assume x_greater_zero: "x > 0" moreover
-    from n_not_zero have "0 < n" by simp moreover
-    have "diff 0 = diff 0" by simp moreover
-    have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-      proof (rule allI, rule allI, rule impI)
-	fix m t
-	assume "m < n & 0 \<le> t & t \<le> x"
-	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp
-      qed
-      ultimately have t_exists:"\<exists>t>0. t < x \<and>
-        diff 0 x =
-        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
-      from this obtain t where t_def: "?P t" ..
-      from t_def x_greater_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
-	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
-	by fastsimp
-      thus ?thesis ..
-    qed
+    assume "x < 0"
+    with `n \<noteq> 0` DERIV
+    have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" by (intro Maclaurin_minus) auto
+    then guess t ..
+    with `x < 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
+    thus ?thesis ..
+  next
+    assume "x > 0"
+    with `n \<noteq> 0` `diff 0 = f` DERIV
+    have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" by (intro Maclaurin) auto
+    then guess t ..
+    with `x > 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
+    thus ?thesis ..
   qed
 qed
 
-
 lemma Maclaurin_all_lt:
   assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
   and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
-  shows "\<exists>t. 0 < abs t & abs t < abs x &
-               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
-                     (diff n t / real (fact n)) * x ^ n" 
-proof -
-  have "(x = 0) \<Longrightarrow> ?thesis"
-  proof -
-    assume "x = 0"
-    with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..
-  qed
-  moreover have "(x < 0) \<Longrightarrow> ?thesis"
-  proof -
-    assume x_less_zero: "x < 0"
-    from DERIV have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp 
-    with x_less_zero INIT2 INIT1 have "\<exists>t>x. t < 0 \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
-    from this obtain t where "?P t" ..
-    with x_less_zero have "0 < \<bar>t\<bar> \<and>
-      \<bar>t\<bar> < \<bar>x\<bar> \<and>
-      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by simp
-    thus ?thesis ..
-  qed
-  moreover have "(x > 0) \<Longrightarrow> ?thesis"
-  proof -
-    assume x_greater_zero: "x > 0"
-    from DERIV have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp
-    with x_greater_zero INIT2 INIT1 have "\<exists>t>0. t < x \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
-    from this obtain t where "?P t" ..
-    with x_greater_zero have "0 < \<bar>t\<bar> \<and>
-      \<bar>t\<bar> < \<bar>x\<bar> \<and>
-      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by fastsimp
-    thus ?thesis ..
-  qed
-  ultimately show ?thesis by (fastsimp) 
+  shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
+    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
+                (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
+proof (cases rule: linorder_cases)
+  assume "x = 0" with INIT3 show "?thesis"..
+next
+  assume "x < 0"
+  with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" by (intro Maclaurin_minus) auto
+  then guess t ..
+  with `x < 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
+  thus ?thesis ..
+next
+  assume "x > 0"
+  with assms have "\<exists>t>0. t < x \<and> f x = ?f x t " by (intro Maclaurin) auto
+  then guess t ..
+  with `x > 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
+  thus ?thesis ..
 qed
 
 
@@ -524,39 +342,30 @@
 lemma Maclaurin_all_le:
   assumes INIT: "diff 0 = f"
   and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
-  shows "\<exists>t. abs t \<le> abs x &
-              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
-                    (diff n t / real (fact n)) * x ^ n"
-proof -
-  note linorder_le_less_linear [of n 0]
-  thus ?thesis
-  proof
-    assume "n\<le> 0" with INIT show ?thesis by force
+  shows "\<exists>t. abs t \<le> abs x & f x =
+    (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
+    (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
+proof cases
+  assume "n = 0" with INIT show ?thesis by force
   next
-    assume n_greater_zero: "n > 0" show ?thesis
-    proof (cases "x = 0")
-      case True
-      from n_greater_zero have "n \<noteq> 0" by auto
-      from True this  have f_0:"(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" by (rule Maclaurin_zero)
-      from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)
-      hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)
-      with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
-       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"
-	by force
-      thus ?thesis ..
-    next
-      case False
-      from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>
-	\<bar>t\<bar> < \<bar>x\<bar> \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_all_lt)
-      from this obtain t where "?P t" ..
-      hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
-       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by (simp add: order_less_le)
-      thus ?thesis ..
-    qed
+  assume "n \<noteq> 0"
+  show ?thesis
+  proof cases
+    assume "x = 0"
+    with `n \<noteq> 0` have "(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
+      by (intro Maclaurin_zero) auto
+    with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
+    thus ?thesis ..
+  next
+    assume "x \<noteq> 0"
+    with INIT `n \<noteq> 0` DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
+      by (intro Maclaurin_all_lt) auto
+    then guess t ..
+    hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
+    thus ?thesis ..
   qed
 qed
 
-
 lemma Maclaurin_all_le_objl: "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
       --> (\<exists>t. abs t \<le> abs x &
@@ -604,7 +413,7 @@
 text{*It is unclear why so many variant results are needed.*}
 
 lemma sin_expansion_lemma:
-     "sin (x + real (Suc m) * pi / 2) =  
+     "sin (x + real (Suc m) * pi / 2) =
       cos (x + real (m) * pi / 2)"
 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 
@@ -635,8 +444,8 @@
                        else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
                        x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
-apply (insert Maclaurin_sin_expansion2 [of x n]) 
-apply (blast intro: elim:); 
+apply (insert Maclaurin_sin_expansion2 [of x n])
+apply (blast intro: elim:)
 done
 
 lemma Maclaurin_sin_expansion3:
@@ -788,7 +597,7 @@
     apply (rule setsum_cong[OF refl])
     apply (subst diff_m_0, simp)
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
-                   simp add: est mult_nonneg_nonneg mult_ac divide_inverse
+                simp add: est mult_nonneg_nonneg mult_ac divide_inverse
                           power_abs [symmetric] abs_mult)
     done
 qed
diff -r 6854e9a40edc -r 5645aaee6b38 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 15:11:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 17:43:22 2010 +0100
@@ -496,7 +496,14 @@
   | group_quant _ Ts t = (Ts, t)
 
 fun dest_weight (@{const SMT.weight} $ w $ t) =
-      (SOME (snd (HOLogic.dest_number w)), t)
+      ((SOME (snd (HOLogic.dest_number w)), t)
+       handle TERM _ =>
+                (case w of
+                  Var ((s, _), _) => (* FIXME: temporary workaround *)
+                    (case Int.fromString s of
+                      SOME n => (SOME n, t)
+                    | NONE => raise TERM ("bad weight", [w]))
+                 | _ => raise TERM ("bad weight", [w])))
   | dest_weight t = (NONE, t)
 
 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
diff -r 6854e9a40edc -r 5645aaee6b38 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 15:11:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 17:43:22 2010 +0100
@@ -539,10 +539,8 @@
           relevant [] [] hopeful
         end
     fun add_facts ths accepts =
-      (facts |> filter ((member Thm.eq_thm ths
-                         andf (not o member (Thm.eq_thm o apsnd snd) accepts))
-                        o snd))
-      @ accepts
+      (facts |> filter (member Thm.eq_thm ths o snd)) @
+      (accepts |> filter_out (member Thm.eq_thm ths o snd))
       |> take max_relevant
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
diff -r 6854e9a40edc -r 5645aaee6b38 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 15:11:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 17:43:22 2010 +0100
@@ -50,6 +50,18 @@
 
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
+  (* for experimentation purposes -- do not use in production code *)
+  val smt_max_iter : int Unsynchronized.ref
+  val smt_iter_fact_frac : real Unsynchronized.ref
+  val smt_iter_time_frac : real Unsynchronized.ref
+  val smt_iter_min_msecs : int Unsynchronized.ref
+  val smt_monomorph_limit : int Unsynchronized.ref
+  val smt_weights : bool Unsynchronized.ref
+  val smt_min_weight : int Unsynchronized.ref
+  val smt_max_weight : int Unsynchronized.ref
+  val smt_max_index : int Unsynchronized.ref
+  val smt_weight_curve : (int -> int) Unsynchronized.ref
+
   val das_Tool : string
   val is_smt_prover : Proof.context -> string -> bool
   val is_prover_available : Proof.context -> string -> bool
@@ -269,6 +281,8 @@
 fun overlord_file_location_for_prover prover =
   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
 
+val atp_first_iter_time_frac = 0.67
+
 (* Important messages are important but not so important that users want to see
    them each time. *)
 val important_message_keep_factor = 0.1
@@ -353,11 +367,12 @@
             val run_twice = has_incomplete_mode andalso not auto
             val timer = Timer.startRealTimer ()
             val result =
-              run false (if run_twice then
-                           Time.fromMilliseconds
-                                         (2 * Time.toMilliseconds timeout div 3)
-                         else
-                           timeout)
+              run false
+                 (if run_twice then
+                    seconds (0.001 * atp_first_iter_time_frac
+                             * Real.fromInt (Time.toMilliseconds timeout))
+                  else
+                    timeout)
               |> run_twice
                  ? (fn (_, msecs0, _, SOME _) =>
                        run true (Time.- (timeout, Timer.checkRealTimer timer))
@@ -437,23 +452,24 @@
   | failure_from_smt_failure _ = UnknownError
 
 (* FUDGE *)
-val smt_max_iter = 8
-val smt_iter_fact_divisor = 2
-val smt_iter_min_msecs = 5000
-val smt_iter_timeout_divisor = 2
-val smt_monomorph_limit = 4
+val smt_max_iter = Unsynchronized.ref 8
+val smt_iter_fact_frac = Unsynchronized.ref 0.5
+val smt_iter_time_frac = Unsynchronized.ref 0.5
+val smt_iter_min_msecs = Unsynchronized.ref 5000
+val smt_monomorph_limit = Unsynchronized.ref 4
 
 fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
   let
     val ctxt = Proof.context_of state
-    fun iter timeout iter_num outcome0 msecs_so_far facts =
+    fun iter timeout iter_num outcome0 time_so_far facts =
       let
         val timer = Timer.startRealTimer ()
         val ms = timeout |> Time.toMilliseconds
         val iter_timeout =
-          if iter_num < smt_max_iter then
-            Int.min (ms, Int.max (smt_iter_min_msecs,
-                                  ms div smt_iter_timeout_divisor))
+          if iter_num < !smt_max_iter then
+            Int.min (ms,
+                Int.max (!smt_iter_min_msecs,
+                    Real.ceil (!smt_iter_time_frac * Real.fromInt ms)))
             |> Time.fromMilliseconds
           else
             timeout
@@ -465,8 +481,10 @@
             |> Output.urgent_message
           else
             ()
-        val {outcome, used_facts, run_time_in_msecs} =
+        val birth = Timer.checkRealTimer timer
+        val {outcome, used_facts, ...} =
           SMT_Solver.smt_filter remote iter_timeout state facts i
+        val death = Timer.checkRealTimer timer
         val _ =
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
@@ -474,7 +492,7 @@
           else
             ()
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
-        val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
+        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
         val too_many_facts_perhaps =
           case outcome of
             NONE => false
@@ -493,16 +511,17 @@
           | SOME _ => true
         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
-        if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso
+        if too_many_facts_perhaps andalso iter_num < !smt_max_iter andalso
            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
-          let val facts = take (num_facts div smt_iter_fact_divisor) facts in
-            iter timeout (iter_num + 1) outcome0 msecs_so_far facts
-          end
+          let
+            val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts)
+          in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end
         else
           {outcome = if is_none outcome then NONE else the outcome0,
-           used_facts = used_facts, run_time_in_msecs = msecs_so_far}
+           used_facts = used_facts,
+           run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
       end
-  in iter timeout 1 NONE (SOME 0) end
+  in iter timeout 1 NONE Time.zeroTime end
 
 (* taken from "Mirabelle" and generalized *)
 fun can_apply timeout tac state i =
@@ -522,7 +541,26 @@
             (Config.put Metis_Tactics.verbose debug
              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
-fun run_smt_solver auto name (params as {debug, overlord, ...}) minimize_command
+val smt_weights = Unsynchronized.ref true
+val smt_weight_min_facts = 20
+
+(* FUDGE *)
+val smt_min_weight = Unsynchronized.ref 0
+val smt_max_weight = Unsynchronized.ref 10
+val smt_max_index = Unsynchronized.ref 200
+val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt_fact_weight j num_facts =
+  if !smt_weights andalso num_facts >= smt_weight_min_facts then
+    SOME (!smt_max_weight
+          - (!smt_max_weight - !smt_min_weight + 1)
+            * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1))
+            div !smt_weight_curve (!smt_max_index))
+  else
+    NONE
+
+fun run_smt_solver auto name (params as {debug, verbose, overlord, ...})
+        minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val (remote, suffix) =
@@ -538,10 +576,16 @@
                         |> (fn (path, base) => path ^ "/" ^ base))
           else
             I)
-      #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
+      #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit)
     val state = state |> Proof.map_context repair_context
     val thy = Proof.theory_of state
-    val facts = facts |> map (apsnd (pair NONE o Thm.transfer thy) o untranslated_fact)
+    val num_facts = length facts
+    val facts =
+      facts ~~ (0 upto num_facts - 1)
+      |> map (fn (fact, j) =>
+                 fact |> untranslated_fact
+                      |> apsnd (pair (smt_fact_weight j num_facts)
+                                o Thm.transfer thy))
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal facts
     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
@@ -561,7 +605,13 @@
               (apply_on_subgoal settings subgoal subgoal_count ^
                command_call method (map fst other_lemmas)) ^
           minimize_line minimize_command
-                        (map fst (other_lemmas @ chained_lemmas))
+                        (map fst (other_lemmas @ chained_lemmas)) ^
+          (if verbose then
+             "\nSMT solver real CPU time: " ^
+             string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^
+             "."
+           else
+             "")
         end
       | SOME failure => string_for_failure "SMT solver" failure
   in