src/HOL/Hyperreal/Transcendental.thy
changeset 20432 07ec57376051
parent 20256 5024ba0831a6
child 20516 2d2e1d323a05
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Aug 29 21:43:34 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Aug 30 03:19:08 2006 +0200
     1.3 @@ -400,6 +400,8 @@
     1.4  apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
     1.5  apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
     1.6  apply (auto simp add: mult_assoc power_abs abs_mult)
     1.7 + prefer 2
     1.8 + apply (drule_tac x = 0 in spec, force)
     1.9  apply (auto simp add: power_abs mult_ac)
    1.10  apply (rule_tac a2 = "z ^ n" 
    1.11         in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
    1.12 @@ -576,6 +578,8 @@
    1.13  
    1.14  text{* FIXME: Long proofs*}
    1.15  
    1.16 +ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proofs *)
    1.17 +
    1.18  lemma termdiffs_aux:
    1.19       "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
    1.20      ==> (\<lambda>h. \<Sum>n. c n *
    1.21 @@ -589,56 +593,53 @@
    1.22       and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
    1.23                               - (real n * (x ^ (n - Suc 0))))" 
    1.24         in lemma_termdiff5)
    1.25 -  -- "3 subgoals"
    1.26 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
    1.27 -  apply (auto simp add: add_commute)
    1.28 - apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
    1.29 -  apply (rule_tac [2] x = K in powser_insidea, auto)
    1.30 - apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
    1.31 -  apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
    1.32 - apply (simp add: diffs_def mult_assoc [symmetric])
    1.33 - apply (subgoal_tac
    1.34 -         "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
    1.35 -               = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
    1.36 -  apply (auto simp add: abs_mult)
    1.37 -   apply (drule diffs_equiv)
    1.38 -   apply (drule sums_summable)
    1.39 -   apply (simp_all add: diffs_def)
    1.40 - apply (simp add: diffs_def mult_ac)
    1.41 - apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
    1.42 -  apply auto
    1.43 +apply (auto simp add: add_commute)
    1.44 +apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
    1.45 +apply (rule_tac [2] x = K in powser_insidea, auto)
    1.46 +apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
    1.47 +apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
    1.48 +apply (simp add: diffs_def mult_assoc [symmetric])
    1.49 +apply (subgoal_tac
    1.50 +        "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
    1.51 +              = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
    1.52 +apply (auto simp add: abs_mult)
    1.53 +apply (drule diffs_equiv)
    1.54 +apply (drule sums_summable)
    1.55 +apply (simp_all add: diffs_def) 
    1.56 +apply (simp add: diffs_def mult_ac)
    1.57 +apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
    1.58 +apply auto
    1.59    prefer 2
    1.60    apply (rule ext)
    1.61 -  apply (simp add: diffs_def)
    1.62 +  apply (simp add: diffs_def) 
    1.63    apply (case_tac "n", auto)
    1.64  txt{*23*}
    1.65     apply (drule abs_ge_zero [THEN order_le_less_trans])
    1.66 -   apply (simp add: mult_ac)
    1.67 +   apply (simp add: mult_ac) 
    1.68    apply (drule abs_ge_zero [THEN order_le_less_trans])
    1.69 -  apply (simp add: mult_ac)
    1.70 +  apply (simp add: mult_ac) 
    1.71   apply (drule diffs_equiv)
    1.72   apply (drule sums_summable)
    1.73 - apply (subgoal_tac
    1.74 -           "summable
    1.75 -             (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
    1.76 -                  r ^ (n - Suc 0)) =
    1.77 -            summable
    1.78 -             (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
    1.79 -  apply simp
    1.80 - apply (rule_tac f = summable in arg_cong, rule ext)
    1.81 +apply (subgoal_tac
    1.82 +          "summable
    1.83 +            (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
    1.84 +                 r ^ (n - Suc 0)) =
    1.85 +           summable
    1.86 +            (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
    1.87 +apply simp 
    1.88 +apply (rule_tac f = summable in arg_cong, rule ext)
    1.89  txt{*33*}
    1.90 - apply (case_tac "n", auto)
    1.91 - apply (case_tac "nat", auto)
    1.92 - apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
    1.93 +apply (case_tac "n", auto)
    1.94 +apply (case_tac "nat", auto)
    1.95 +apply (drule abs_ge_zero [THEN order_le_less_trans], auto) 
    1.96  apply (drule abs_ge_zero [THEN order_le_less_trans])
    1.97  apply (simp add: mult_assoc)
    1.98  apply (rule mult_left_mono)
    1.99 - prefer 2 apply arith
   1.100 + prefer 2 apply arith 
   1.101  apply (subst add_commute)
   1.102  apply (simp (no_asm) add: mult_assoc [symmetric])
   1.103  apply (rule lemma_termdiff3)
   1.104 -  apply (auto intro: abs_triangle_ineq [THEN order_trans])
   1.105 -apply arith
   1.106 +apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
   1.107  done
   1.108  
   1.109  ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   1.110 @@ -655,7 +656,7 @@
   1.111  apply (simp add: LIM_def, safe)
   1.112  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
   1.113  apply (auto simp add: less_diff_eq)
   1.114 -apply (frule abs_triangle_ineq [THEN order_le_less_trans])
   1.115 +apply (drule abs_triangle_ineq [THEN order_le_less_trans])
   1.116  apply (rule_tac y = 0 in order_le_less_trans, auto)
   1.117  apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (\<Sum>n. (c n) * (x ^ n)) & (%n. (c n) * ((x + xa) ^ n)) sums (\<Sum>n. (c n) * ( (x + xa) ^ n))")
   1.118  apply (auto intro!: summable_sums)
   1.119 @@ -667,11 +668,11 @@
   1.120  apply (simp add: diff_def divide_inverse add_ac mult_ac)
   1.121  apply (rule LIM_zero_cancel)
   1.122  apply (rule_tac g = "%h. \<Sum>n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))" in LIM_trans)
   1.123 - prefer 2 apply (blast intro: termdiffs_aux)
   1.124 + prefer 2 apply (blast intro: termdiffs_aux) 
   1.125  apply (simp add: LIM_def, safe)
   1.126  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
   1.127  apply (auto simp add: less_diff_eq)
   1.128 -apply (frule abs_triangle_ineq [THEN order_le_less_trans])
   1.129 +apply (drule abs_triangle_ineq [THEN order_le_less_trans])
   1.130  apply (rule_tac y = 0 in order_le_less_trans, auto)
   1.131  apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
   1.132  apply (rule_tac [2] powser_inside, auto)
   1.133 @@ -2580,5 +2581,5 @@
   1.134  apply (drule_tac [3] LIM_fun_gt_zero)
   1.135  apply force+
   1.136  done
   1.137 -
   1.138 +  
   1.139  end