# HG changeset patch
# User webertj
# Date 1154231590 -7200
# Node ID 5024ba0831a63f9ac85e2191dff161500e976b30
# Parent  5a8410198a33dd4f68b9890ac547e01c7b57ea77
lin_arith_prover splits certain operators (e.g. min, max, abs)

diff -r 5a8410198a33 -r 5024ba0831a6 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Sun Jul 30 05:53:10 2006 +0200
@@ -764,8 +764,10 @@
 apply (subgoal_tac "0 < v")
  prefer 2 apply arith
 apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
-apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
 apply (simp add: power2_eq_square)
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+apply (rule_tac lemma_sqrt_hcomplex_capprox, auto)
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 done
 
 lemma CFinite_HFinite_iff:
diff -r 5a8410198a33 -r 5024ba0831a6 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Sun Jul 30 05:53:10 2006 +0200
@@ -173,7 +173,10 @@
  prefer 2 apply assumption
 apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
  prefer 2 apply arith
-apply (drule_tac x = "psize D - Suc n" in spec, simp) 
+apply (drule_tac x = "psize D - Suc n" in spec)
+ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
+apply simp
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 done
 
 lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
@@ -436,6 +439,8 @@
 apply (simp add: right_diff_distrib)
 done
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
              ==> Integral(a,b) f' (f(b) - f(a))"
 apply (drule order_le_imp_less_or_eq, auto) 
@@ -467,6 +472,7 @@
           fine_def)
 done
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
 by simp
diff -r 5a8410198a33 -r 5024ba0831a6 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Sun Jul 30 05:53:10 2006 +0200
@@ -394,7 +394,7 @@
   apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
   apply force
   apply assumption
-  apply (simp add: power2_eq_square mult_compare_simps)
+  apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
   apply (rule mult_imp_div_pos_less)
   apply (rule mult_pos_pos, assumption, assumption)
   apply (subgoal_tac "xa * xa = abs xa * abs xa")
@@ -408,6 +408,7 @@
   apply (subst diff_minus [THEN sym])+
   apply (subst ln_div [THEN sym])
   apply arith
+  apply assumption
   apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq 
     add_divide_distrib power2_eq_square)
   apply (rule mult_pos_pos, assumption)+
diff -r 5a8410198a33 -r 5024ba0831a6 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Sun Jul 30 05:53:10 2006 +0200
@@ -425,7 +425,7 @@
 lemma poly_add_length [rule_format]:
      "\<forall>p2. length (p1 +++ p2) =
              (if (length p1 < length p2) then length p2 else length p1)"
-apply (induct "p1", simp_all, arith)
+apply (induct "p1", simp_all)
 done
 
 lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
diff -r 5a8410198a33 -r 5024ba0831a6 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun Jul 30 05:53:10 2006 +0200
@@ -400,8 +400,6 @@
 apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
 apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
 apply (auto simp add: mult_assoc power_abs abs_mult)
- prefer 2
- apply (drule_tac x = 0 in spec, force)
 apply (auto simp add: power_abs mult_ac)
 apply (rule_tac a2 = "z ^ n" 
        in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
@@ -578,8 +576,6 @@
 
 text{* FIXME: Long proofs*}
 
-ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}  (* FIXME: rewrite proofs *)
-
 lemma termdiffs_aux:
      "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
     ==> (\<lambda>h. \<Sum>n. c n *
@@ -593,56 +589,59 @@
      and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
                              - (real n * (x ^ (n - Suc 0))))" 
        in lemma_termdiff5)
-apply (auto simp add: add_commute)
-apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
-apply (rule_tac [2] x = K in powser_insidea, auto)
-apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
-apply (simp add: diffs_def mult_assoc [symmetric])
-apply (subgoal_tac
-        "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
-              = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
-apply (auto simp add: abs_mult)
-apply (drule diffs_equiv)
-apply (drule sums_summable)
-apply (simp_all add: diffs_def) 
-apply (simp add: diffs_def mult_ac)
-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))")
-apply auto
+  -- "3 subgoals"
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+  apply (auto simp add: add_commute)
+ apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
+  apply (rule_tac [2] x = K in powser_insidea, auto)
+ apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
+  apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
+ apply (simp add: diffs_def mult_assoc [symmetric])
+ apply (subgoal_tac
+         "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
+               = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
+  apply (auto simp add: abs_mult)
+   apply (drule diffs_equiv)
+   apply (drule sums_summable)
+   apply (simp_all add: diffs_def)
+ apply (simp add: diffs_def mult_ac)
+ 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))")
+  apply auto
   prefer 2
   apply (rule ext)
-  apply (simp add: diffs_def) 
+  apply (simp add: diffs_def)
   apply (case_tac "n", auto)
 txt{*23*}
    apply (drule abs_ge_zero [THEN order_le_less_trans])
-   apply (simp add: mult_ac) 
+   apply (simp add: mult_ac)
   apply (drule abs_ge_zero [THEN order_le_less_trans])
-  apply (simp add: mult_ac) 
+  apply (simp add: mult_ac)
  apply (drule diffs_equiv)
  apply (drule sums_summable)
-apply (subgoal_tac
-          "summable
-            (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
-                 r ^ (n - Suc 0)) =
-           summable
-            (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
-apply simp 
-apply (rule_tac f = summable in arg_cong, rule ext)
+ apply (subgoal_tac
+           "summable
+             (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
+                  r ^ (n - Suc 0)) =
+            summable
+             (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
+  apply simp
+ apply (rule_tac f = summable in arg_cong, rule ext)
 txt{*33*}
-apply (case_tac "n", auto)
-apply (case_tac "nat", auto)
-apply (drule abs_ge_zero [THEN order_le_less_trans], auto) 
+ apply (case_tac "n", auto)
+ apply (case_tac "nat", auto)
+ apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
 apply (drule abs_ge_zero [THEN order_le_less_trans])
 apply (simp add: mult_assoc)
 apply (rule mult_left_mono)
- prefer 2 apply arith 
+ prefer 2 apply arith
 apply (subst add_commute)
 apply (simp (no_asm) add: mult_assoc [symmetric])
 apply (rule lemma_termdiff3)
-apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
+  apply (auto intro: abs_triangle_ineq [THEN order_trans])
+apply arith
 done
 
-ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma termdiffs: 
     "[| summable(%n. c(n) * (K ^ n));  
@@ -656,7 +655,7 @@
 apply (simp add: LIM_def, safe)
 apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
 apply (auto simp add: less_diff_eq)
-apply (drule abs_triangle_ineq [THEN order_le_less_trans])
+apply (frule abs_triangle_ineq [THEN order_le_less_trans])
 apply (rule_tac y = 0 in order_le_less_trans, auto)
 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))")
 apply (auto intro!: summable_sums)
@@ -668,11 +667,11 @@
 apply (simp add: diff_def divide_inverse add_ac mult_ac)
 apply (rule LIM_zero_cancel)
 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)
- prefer 2 apply (blast intro: termdiffs_aux) 
+ prefer 2 apply (blast intro: termdiffs_aux)
 apply (simp add: LIM_def, safe)
 apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
 apply (auto simp add: less_diff_eq)
-apply (drule abs_triangle_ineq [THEN order_le_less_trans])
+apply (frule abs_triangle_ineq [THEN order_le_less_trans])
 apply (rule_tac y = 0 in order_le_less_trans, auto)
 apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
 apply (rule_tac [2] powser_inside, auto)
@@ -2581,5 +2580,5 @@
 apply (drule_tac [3] LIM_fun_gt_zero)
 apply force+
 done
-  
+
 end